Logic in Computer Science (LICS 1990)

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

Authors: Comon, H.

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{Comon-Solvinginequationsi,
    author = 	 {Comon, H.},
    title = 	 {Solving inequations in terms algebras},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {62--69},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }