Model Completeness for Rational Trees
Silvio Ghilardi, Lia M. Poidomani · Lecture notes in computer science · 2024
Abstract We analyze the theory of rational trees with finitely many constructors, infinitely many atoms and an atomicity predicate. We design a new decision procedure, proving in addition that this theory is model-complete. We also show that the enrichment of the language with selectors and simultaneous parametric fixpoints enjoys quantifier elimination.