Next: Version 2.0 (April 1995)
Up: Release Notes
Previous: Version 2.2 (June 1995)
Contents
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