Proof Lengths for Equational Completion

David A. Plaisted
University of North Carolina at Chapel Hill 
Chapel Hill, NC 27599-3175, USA
E-mail: plaisted@cs.unc.edu

Andrea Sattler-Klein
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, GERMANY
E-mail: sattler@informatik.uni-kl.de

Abstract
We first show that ground term-rewriting systems can be completed in a
polynomial number of rewriting steps, if the appropriate data
structure for terms is used.  We then apply this result to study the
lengths of critical pair proofs in non-ground systems, and obtain
bounds on the lengths of critical pair proofs in the non-ground case.
We show how these bounds depend on the types of inference steps that
are allowed in the proofs.

Keywords
completion, term rewriting, proof length, ground systems

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1995/
file: Sattler.SR-95-06.ps.gz