Abstract
We study ground confluence and inductive validity in equational specifications that are interpreted in a constructor based way. By defining semantics of the specification in an appropriate way, we are able to transfer the proof-byconsistency concepts from unstructured specifications to constructor based specifications, where the unstructured specifications with their usual semantics are included as a special case. We further show that the proof-by-consistency concepts not only apply to inductive theorem proving, but can as well be employed to prove ground confluence of rewrite systems. So we present a refutationally complete prover for ground confluence and inductive validity that applies to unstructured as well as constructor based equational specifications.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. Avenhaus and K. Becker, Conditional rewriting modulo a built-in algebra, SEKI Report SR-92-11.
J. Avenhaus and K. Madlener, Term rewriting and equational reasoning, in: R. B. Banerji, ed., Formal Techniques in Artificial Intelligence (North-Holland, Amsterdam, 1990) pp. 1–43.
L. Bachmair, Proof by Consistency in Equational Theories, in: 3rd LICS (1988) pp. 228–233.
R.S. Boyer and J.S. Moore, A Computational Logic (Academic Press, New York, 1979).
R. Burstall, Proving properties of programs by structural induction, Computer Journal 12 (1969) pp. 41–48.
N. Dershowitz and J. P. Jouannaud, Rewriting systems, in: J. van Leeuwen, ed., Handbook of Theoretical Computer Science, Vol. B (Elsevier, Amsterdam, 1990) pp. 241–320.
L. Fribourg, A strong restriction of the inductive completion procedure, 13th ICALP 86, LNCS 266 (Springer, Berlin, 1991) pp. 105–115.
R. Göbel, Ground confluence, in: 2nd RTA 87 LNCS 256 (Springer, Berlin, 1991) pp. 156–167.
G. Huet and J. M. Hullot, Proofs by Induction in Equational Theories with Constructors, J. Comput. Syst. Sci 25 (1982) pp. 239–266.
S. Kaplan and M. Choquer, On the decidability of quasi-reducability, in: Bull. EATCS 28 (1986) pp. 32–34.
D. Kapur and D.R. Musser, Inductive reasoning for incomplete specifications, in: Proc. IEEE Symposium on Logic in Computer Science (Cambridge MA, 1986) pp. 367–377.
D. Kapur and D.R. Musser, Proof by consistency, Artificial Intelligence 31(2) (1987) pp. 125–157.
D. Kapur, P. Narendran and H. Zhang, On sufficient completeness and related properties of term rewriting systems, Acta Informatica 24(4) (1987), pp. 395–415.
D. Kapur, P. Narendran and H. Zhang, Automating inductionless induction using test sets, J. Symbolic Computation 11 (1991), pp. 83–111.
E. Kounalis and M. Rusinowitch, Mechanizing Inductive Reasoning, in: Proc. of 8th AAAI '90 (MIT Press, 1990) pp. 240–245.
O. Lysne, Proof by consistency in constructive systems with final algebra semantics, in: Proc. of 3rd ALP '92, LNCS 632, (Springer, Berlin 1992) pp. 276–290.
D. R. Musser, On Proving Inductive Properties of Abstract Data Types, in: Proc. 7th ACM Symp. on Principles of Programming Languages (1980) pp. 154–162.
W. Nutt, P. Réty and G. Smolka, Basic narrowing revisited, Journal of Symbolic Computation 7(3 & 4) 1989, pp. 295–318.
P. Padawitz, Generic induction proofs, to appear in CTRS 92.
D. Plaisted, Semantic confluence tests and completion methods, Inform, and Control 65(2/3) 1985, pp. 182–215.
G. Smolka, W. Nutt, J.A. Goguen and J. Meseguer, Order-sorted equational computation, in: H. Ait-Kaci and M. Nivat, eds., Resolution of Equations in Algebraic Structures, Vol. 2 (Academic Press, San Diego CA, 1989) pp. 297–367.
C.-P. Wirth, Inductive theorem proving in theories specified by positive/negative conditional equations, Diplomarbeit, Universität Kaiserslautern, Fachbereich Informatik, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Becker, K. (1993). Proving ground confluence and inductive validity in constructor based equational specifications. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_55
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_55
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive