摘要翻译：
本文给出了有限树或无限树的一个推广理论t$的一阶公理化，它建立在包含无穷个函数符号集的签名和一个能区分有限树或无限树的关系式$\fini(t)$上。我们证明了$T$至少有一个模型，并证明了它的完备性，不仅给出了一个决策过程，而且给出了一个完整的一阶约束求解器，它对$T$中的任何一阶约束满足问题都给出了明确的解。求解器是以16条重写规则的形式给出的，这些规则将任何一阶约束$\phi$转换为简单公式的等效析取$\phi$,使得$\phi$要么是公式$\true$,要么是公式$\false$,或者是至少有一个自由变量的公式，既不等效于$\true$,也不等效于$\false$,其中自由变量的解以明确的方式表示。我们规则的正确性意味着$T$的完整性。我们还描述了我们的算法在CHR（约束处理规则）中的实现，并与C++中的实现以及最近的可分解理论决策过程的实现进行了比较。
---
英文标题：
《Theory of Finite or Infinite Trees Revisited》
---
作者：
Khalil Djelloul, Thi-bich-hanh Dao and Thom Fruehwirth
---
最新提交年份：
2007
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Logic in Computer Science        计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  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.
---
PDF链接：
https://arxiv.org/pdf/0706.4323