## Paper: Solving inequations in terms algebras (at LICS 1990)

**Hubert Comon-Lundh**

### Abstract

Let T be the theory of term algebra over the relational symbols = or ≥, where ≥ is interpreted as a lexicographic path ordering. The decidability of the purely existential fragment of T is shown. The proof is carried out in three steps. The first step consists of the transformation of any quantifier-free formula φ (i.e. all variables are free) into a solved form that has the same set of solutions as φ. Then the author shows how to decide the satisfiability of some particular problems called simple systems. A simple system is a formula which defines a total ordering on the terms occurring in it and which is closed under deduction. This last property means that if ψ is a solved form of a simple system φ then ψ must be a subformula of φ. The proof is completed by showing how to reduce the satisfiability of an arbitrary solved form to the satisfiability of finitely many simple systems

### BibTeX

@InProceedings{ComonLundh-Solvinginequationsi, author = {Hubert Comon-Lundh}, title = {Solving inequations in terms algebras}, booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)}, year = {1990}, month = {June}, pages = {62--69}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }