Quantifier elimination for infinite terms (Q1812980)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Quantifier elimination for infinite terms |
scientific article |
Statements
Quantifier elimination for infinite terms (English)
0 references
25 June 1992
0 references
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.
0 references
theory of infinite terms
0 references
complete extensions
0 references
decision procedure
0 references
effective quantifier elimination procedure
0 references