IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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

Authors: Hubert Comon-Lundh


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


    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}

Last modified: 2018-06-2121:59
Andrzej Murawski