Steklov Institute of Mathematics at St.Petersburg

PREPRINT 09/2004

FIRST REPORT ON THE SEMIALGEBRAIC PROVER

This preprint was accepted July 30, 2004

ABSTRACT:
We describe the basic notions and the algorithm of the semialgebraic
prover being developed in Laboratory of Mathematical Logic of Steklov
Insitute of Mathematics at St.Petersburg.  The prover solves formulas of
the first-order logic (with emphasis on formulas having hard
propositional part) by translating them into systems of inequalities and
searching for a semialgebraic refutation of these systems. 

The prover is written in C++.  The implementation is flexible and allows
to modify easily the rules of proof system and even the nature of
derivation objects.