Theory of Finite or Infinite Trees Revisited

Details Theory of Finite or Infinite Trees Revisited Theory of Finite or Infinite Trees Revisited

2007-06-28

arxiv.org/abs/0706.4323v1

Computer Science

Logic in Computer Science

Scientific paper

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 $\phi$ into an equivalent disjunction $\phi$ of simple formulas such that $\phi$ 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.

Affiliated with

Also associated with

No associations

Rating

Theory of Finite or Infinite Trees Revisited does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Theory of Finite or Infinite Trees Revisited, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Theory of Finite or Infinite Trees Revisited will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-681408