Abstract
The paper presents a new completion procedure for conditional equations. The work is based on the notion of reductive conditional rewriting. The procedure has been designed to also handle nonreductive equations that are generated during completion. The paper in particular presents techniques for simplification of conditional equations and rules, so that the procedure terminates on more specifications. The correctness proofs which form a substantial part of this paper employ recursive path orderings on proof trees, an extension of the ideas of Bachmair, Dershowitz and Hsiang to the conditional case.
Cite
CITATION STYLE
Ganzinger, H. (1988). A completion procedure for conditional equations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 308 LNCS, pp. 62–83). Springer Verlag. https://doi.org/10.1007/3-540-19242-5_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
