Abstract
We discuss the conditional rewriting aspects of the Focus program transformation/synthesis system. The term-rewriting induction principle, presented earlier for unconditional rewrite systems, is generalized for conditional systems. We also present a novel deduction method for first-order clauses called contextual deduction which may be considered to be the first-order analogue of the rewriting operation. Like rewriting, contextual deduction uses pattern matching instead of unification and has the property of finite termination. We identify a sufficient condition for clausal theories, called saturation, under which contextual deduction is complete for refuting ground goal clauses.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
L. Bachmair. Proof normalization for resolution and paramodulation. In N. Dershowitz, editor, Rewriting Techniques and Appl., pages 15–28, Springer-Verlag, Berlin, 1989. (Lecture Notes in Comp. Science, Vol 355).
F. Bronsard and U. S. Reddy. An axiomatization of a functional logic language. In Algebraic and Logic Programming, pages 101–116, Springer-Verlag, Oct 1990. (LNCS Vol. 463).
N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.
L. Fribourg. A strong restriction of the inductive completion procedure. In Intern. Conf. Aut., Lang. and Program., pages 105–115, Rennes, France, July 1986. (Springer Lecture Notes in Computer Science, Vol. 226).
M.-C. Gaudel and S. Kaplan. How to build meaningful algebraic specification. ESPRIT Meteor Project Technical report, Orsay-France, 1986.
G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. In Symp. on Foundations of Computer Science, pages 96–107, IEEE, Lake Placid, NY, October 1980.
Jieh Hsiang and Michaël Rusinowitch. A new method for establishing refutational completeness in theorem proving. In J. H. Siekmann, editor, Proceedings of the Eighth International Conference on Automated Deduction; pages 141–152, Oxford, England, July 1986. Vol. 230 of Lecture Notes in Computer Science, Springer, Berlin.
J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in equational theories without constructors. In Symp. on Logic in Computer Science, pages 358–366, IEEE, Cambridge, MA., June 1986.
S. Kaplan. Simplifying conditional term rewriting systems: Unification, termination and confluence. J. of Symbolic Computation, 4:295–334, 1987.
D. Kapur, P. Narendran, and H. Zhang. Proof by induction using test sets. In Conf. on Automated Deduction, Oxford, U.K., 1986.
E. Kounalis and M. Rusinowitch. On word problems in Horn theories. In S. Kaplan and J.-P. Jouannaud, editors, Conditional Term Rewriting Systems, pages 144–160, Springer-Verlag, Berlin, 1987. (LNCS Vol 308).
D. R. Musser. On proving inductive properties of abstract data types. In ACM Symp. on Princ. of Program. Languages, pages 154–162, ACM, Las Vegas, 1980.
U. S. Reddy. Functional logic languages, Part I. In Graph Reduction, pages 401–425, Springer-Verlag, 1987. (Lecture Notes in Computer Science, Vol 279).
U. S. Reddy. Transformational derivation of programs using the Focus system. In Symp. Practical Software Development Environments, pages 163–172, ACM, December 1988.
U. S. Reddy. Rewriting techniques for program synthesis. In N. Dershowitz, editor, Rewriting Techniques and Appl., pages 388–403, Springer-Verlag, 1989. (LNCS Vol. 355).
U. S. Reddy. Term rewriting induction. In M. Stickel, editor, Conf. on Automated Deduction, pages 162–177, Springer-Verlag, 1990. (Lecture Notes in Artificial Intelligence, Vol. 449).
Michaël Rusinowitch. Démonstration Automatique: Techniques de réécriture. InterEditions, Paris, France, 1989.
Sivakumar. Conditional Rewriting. PhD thesis, UIUC, 1988.
H. Zhang and D. Kapur. First-order theorem proving using conditional rewrite rules. In E. Lusk and R. Overbeek, editors, Conf. on Automated Deduction, pages 1–20, Springer-Verlag, Berlin, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bronsard, F., Reddy, U.S. (1991). Conditional rewriting in focus. In: Kaplan, S., Okada, M. (eds) Conditional and Typed Rewriting Systems. CTRS 1990. Lecture Notes in Computer Science, vol 516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54317-1_77
Download citation
DOI: https://doi.org/10.1007/3-540-54317-1_77
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54317-6
Online ISBN: 978-3-540-47558-3
eBook Packages: Springer Book Archive