Abstract
The techniques of clausal rewriting and clausal completion provide several theorem proving methods in theories expressed by clauses having at most one positive equality literal and without negative equality literals. The clausal completion procedure consists of a form of ordered superposition, combined with the powerful clausal rewriting technique for simplification and deletion of redundant axioms, and has been described and proved correct in [NO90]. In this note we outline several applications of these techniques, such as efficient prototyping, checking sufficient completeness properties and theorem proving in partial specifications. Furthermore, some methods used in the implementation of these techniques are described and their correctness is proved.
This work has been partially supported by the ESPRIT Project PROSPECTRA ref. no. 390, under subcontract with Alcatel SESA.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
9. References
E. Astesiano, M. Ceroli. On the existence of initial models for partial (high-order) conditional specifications, in Proc. TAPSOFT '89, vol 1, J. Diaz, F. Orejas (eds.) Springer Lect. Notes in Comp. Sc. 351 (1989) pp. 74–88.
L. Bachmair, N. Dershowitz, J. Hsiang: Orderings for equational proofs. In Proc. Symp. Logic in Computer Science, 346–357, Boston (Massachusetts USA), 1986.
L. Bachmair, H. Ganzinger: On restrictions of ordered paramodulation with simplification. In Proc. 10th Int. Conf. on Automated Deduction. LNCS. To appear.
L. Bachmair, H. Ganzinger: Completion of First Order Clauses with Equality By Strict Superposition. To appear in proc. Second Int. Workshop on Conditional and Typed Term Rewriting. LNCS, 1990.
W. Bousdira, J-L. Remy: On sufficient Completeness of Conditional Specifications. To appear in proc. Second Int. Workshop on Conditional and Typed Term Rewriting. LNCS, 1990.
N. Dershowitz: Termination of rewriting. Journal of Symbolic Computation, 69–116, 1987.
H. Ganzinger, R. Schäfers: System support for order-sorted Horn clause specifications. In Proc. 12th Int. Conf. on Software Engineering. Nice. pp. 150–159. 1990.
J. Hsiang, M. Rusinowitch: Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Submitted for publication.
D.E. Knuth, P.B. Bendix: Simple word problems in universal algebras. J. Leech, editor, Computational Problems in Abstract Algebra, 263–297, Pergamon Press, Oxford, 1970.
S. Kaplan: Fair conditional term rewriting systems: unification, termination and confluence. Recent Trends in Data Type Specification, Springer IFB 116 (1985).
D. Kapur, P. Narendran, G. Sivakumar: A path Ordering for Proving Termination of Term Rewrite Systems. LNCS 186, 173–187, 1985.
R. Nieuwenhuis, F. Orejas, A. Rubio: TRIP: an implementation of clausal rewriting. In Proc. 10th Int. Conf. on Automated Deduction. Kaiserslautern 1990, LNCS 449, pp 667–668.
R. Nieuwenhuis, F. Orejas: Clausal Completion. To appear in proc. Second Int. Workshop on Conditional and Typed Term Rewriting. (LNCS) Montreal 1990.
R. Nieuwenhuis: Theorem proving in first order logic with equality by clausal rewriting and completion. PhD thesis, UPC Barcelona, 1990.
M. Navarro, P. Nivela, F. Orejas, A. Sánchez: Translating partial into total specifications, Research Report LSI-89-21 Dept. Lenguajes y Sistemas Informáticos, UPC, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nieuwenhuis, R., Orejas, F. (1991). Clausal rewriting: Applications and implementation. In: Ehrig, H., Jantke, K.P., Orejas, F., Reichel, H. (eds) Recent Trends in Data Type Specification. ADT 1990. Lecture Notes in Computer Science, vol 534. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54496-8_11
Download citation
DOI: https://doi.org/10.1007/3-540-54496-8_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54496-8
Online ISBN: 978-3-540-38416-8
eBook Packages: Springer Book Archive