Theory of finite or infinite trees revisited

9 years 9 months ago
Theory of finite or infinite trees revisited
We present in this paper a first-order axiomatization of an extended theory T of finite or infinite trees, built on a signature containing an infinite set of function symbols and a relation finite(t) which enables to distinguish between finite or infinite trees. We show that T has at least one model and prove its completeness by giving not only a decision procedure, but a full first-order constraint solver which gives clear and explicit solutions for any first-order constraint satisfaction problem in T. The solver is given in the form of 16 rewriting rules which transform any first-order constraint into an equivalent disjunction of simple formulas such that is either the formula true or the formula false or a formula having at least one free variable, being equivalent neither to true nor to false and where the solutions of the free variables are expressed in a clear and explicit way. The correctness of our rules implies the completeness of T. We also describe an implementation of ou...
Khalil Djelloul, Thi-Bich-Hanh Dao, Thom W. Fr&uum
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TPLP
Authors Khalil Djelloul, Thi-Bich-Hanh Dao, Thom W. Frühwirth
Comments (0)