UCAM-CL-TR-567: Using inequalities as term ordering constraints

Publication announcement:

    Using inequalities as term ordering constraints

    Joe Hurd

    Technical report UCAM-CL-TR-567, University of Cambridge,
    Computer Laboratory, June 2003, 17 pages.

This document is now available at

    http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-567.pdf

Abstract:

In this paper we show how linear inequalities can be used to approximate
Knuth-Bendix term ordering constraints, and how term operations such as
substitution can be carried out on systems of inequalities. Using this
representation allows an off-the-shelf linear arithmetic decision
procedure to check the satisfiability of a set of ordering constraints.
We present a formal description of a resolution calculus where systems
of inequalities are used to constrain clauses, and implement this using
the Omega test as a satisfiability checker. We give the results of an
experiment over problems in the TPTP archive, comparing the practical
performance of the resolution calculus with and without inherited
inequality constraints.

-- 
University of Cambridge, Computer Laboratory,
Technical Reports (ISSN 1476-2986)
http://www.cl.cam.ac.uk/TechReports/