Quantifier elimination for infinite terms

We consider the theory \({\mathcal T}_{IT}\) of infinite terms. The axioms for the theory \({\mathcal T}_{IT}\) are analogous to the Mal'cev's axioms for the theory \({\mathcal T}_{FT}\) of finite terms whose models are the locally free algebras. Recently M. J. Maher has proved that the theory \({\mathcal T}_{IT}\) in a finite non-singular signature plus the Domain Closure Axiom is complete. In this paper, a description of all the complete extensions of \({\mathcal T}_{IT}\) is given and hence an effective decision procedure for \({\mathcal T}_{IT}\) is obtained. The approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theory \({\mathcal T}_{IT}\) can be carried out in analogy with Mal'cev's analysis of \({\mathcal T}_{FT}\). The results follow from an effective quantifier elimination procedure for formulas with pointers.

Recommendations

Cites work

Cited in

(6)

This page was built for publication: Quantifier elimination for infinite terms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1812980)