next up previous contents
Next: Version 2.0 (April 1995) Up: Release Notes Previous: Version 2.2 (June 1995)   Contents

Version 2.1 (May 1995)

We have added a constraint solver for the (lexicographic extension to atoms of the) subterm ordering. This ordering should be used when trying to apply Saturate for proving the locality of certain theories, (cf. subdirectory LocalTheories of saturate/examples). Finitely saturating a theory under this (partial) ordering (actually one saturates with respect to an arbitrary completion of that ordering) proves that the entailment problem for the respective theory is decidable in polynomial time if the theory is Horn, and in CoNP, if it is not Horn. The paper (Basin & Ganzinger, 1996) explains the details.



Harald Ganzinger 2002-12-04

Imprint | Data Protection