## Formalization of Tarski's Theorem

Tarski's Theorem is a generalization of Sturm's
theorem that
provides a linear relationship between functions known as Tarski
queries and cardinalities of certain sets.
The linear system that results from this relationship is in fact invertible and can
be used to explicitly count the number of roots of a
univariate polynomial on a set defined by a system of polynomial
relations. This computation is
used to define a computable function that calculates whether any system of
univariate polynomials is satisfiable.
The PVS contribution `Tarski`

, which is part of the NASA PVS Library,
includes a formalization of Tarski's Theorem, as well as a decision
procedure that determines the
satisfiability of a system of univariate polynomial relations over the real line. It is formally verified in PVS that the
decision procedure is sound and complete.
This result is a the basis of the proof-producing
strategy `tarski`

for reasoning about systems of univariate polynomial
relations on the real line. The soundness of the strategy depends solely on the internal logic of PVS
rather than on an external oracle.

### PVS Contribution

`Tarski`

: Formalization of Tarski's theorem and PVS strategies (see dependency graph).
Strategy `tarski`

: Automatically discharges systems of
polynomial relations.
Examples.
Sturm's Theorem.
### Publications

- Anthony Narkawicz, César Muñoz, and Aaron Dutle,
*
Formally-Verified Decision Procedures for Univariate Polynomial
Computation Based on Sturm’s and Tarski’s Theorems*, Journal
of Automated Reasoning, Volume 54, Issue 4, pp. 285-326, 2015. DOI: 10.1007/s10817-015-9320-x. BibTeX Reference.
- Anthony Narkawicz and César Muñoz,
*A
Formally-Verified Decision Procedure for Univariate Polynomial
Computation Based on Sturm’s Theorem*, Technical Memorandum, NASA/TM-2014-218548, November
2014. BibTeX Reference.

The tag

identifies links that are outside
the NASA domain