Theory of Finite or Infinite Trees Revisited
| dc.creator | Djelloul, Khalil | |
| dc.creator | Dao, Thi-bich-hanh | |
| dc.creator | Fruehwirth, Thom | |
| dc.date | 2007-06-28 | |
| dc.date.accessioned | 2026-07-07T08:13:04Z | |
| dc.date.available | 2026-07-07T08:13:04Z | |
| dc.description | 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 $\fini(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 our algorithm in CHR (Constraint Handling Rules) and compare the performance with an implementation in C++ and that of a recent decision procedure for decomposable theories. | |
| dc.identifier | https://arxiv.org/abs/0706.4323 | |
| dc.identifier | http://arxiv.org/abs/0706.4323 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/132671 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Artificial Intelligence | |
| dc.subject | F.4.1 | |
| dc.title | Theory of Finite or Infinite Trees Revisited | |
| dc.type | text |