Technical reports

Using inequalities as term ordering constraints

Joe Hurd

June 2003, 17 pages

DOI: 10.48456/tr-567

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.

Full text

PDF (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-567,
  author =	 {Hurd, Joe},
  title = 	 {{Using inequalities as term ordering constraints}},
  year = 	 2003,
  month = 	 jun,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-567.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-567},
  number = 	 {UCAM-CL-TR-567}
}