We analyze the theory of rational trees with finitely many construc- tors, 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.
Model Completeness for Rational Trees / S. Ghilardi, L.M. Poidomani (LECTURE NOTES IN COMPUTER SCIENCE). - In: Automated Reasoning / [a cura di] C. Benzmüller, M.J.H. Heule, R.A. Schmidt. - [s.l] : Springer, 2024. - ISBN 978-3-031-63497-0. - pp. 265-283 (( Intervento presentato al 12. convegno IJCA tenutosi a Nancy nel 2024 [10.1007/978-3-031-63498-7_16].
Model Completeness for Rational Trees
S. Ghilardi
;
2024
Abstract
We analyze the theory of rational trees with finitely many construc- tors, 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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
Model_Completeness_for_Rational_Trees.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
274.42 kB
Formato
Adobe PDF
|
274.42 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
