Proof Lengths for Equational Completion
- We first show that ground term-rewriting systems can be completed in apolynomial number of rewriting steps, if the appropriate data structure for termsis used. We then apply this result to study the lengths of critical pair proofs innon-ground systems, and obtain bounds on the lengths of critical pair proofsin the non-ground case. We show how these bounds depend on the types ofinference steps that are allowed in the proofs.
Author: | Andrea Sattler-Klein, David Plaisted |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-3479 |
Series (Serial Number): | SEKI Report (95,6) |
Document Type: | Preprint |
Language of publication: | English |
Year of Completion: | 1999 |
Year of first Publication: | 1999 |
Publishing Institution: | Technische Universität Kaiserslautern |
Date of the Publication (Server): | 2000/04/03 |
Faculties / Organisational entities: | Kaiserslautern - Fachbereich Informatik |
DDC-Cassification: | 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik |
Licence (German): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |