Abstract
We propose a specification language for the formalization of data types with partial or non-terminating operations as part of a rewrite-based framework for inductive theorem proving. The language requires constructors for designating data items and admits positive/negative conditional equations as axioms in specifications. The (total algebra) semantics for such specifications is based on so-called data models. We develop admissibility conditions that guarantee the unique existence of a distinguished data model. Since admissibility of a specification requires confluence of the induced rewrite relation, we provide an effectively testable confluence criterion which does not presuppose termination.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. Avenhaus and K. Madlener. Theorem proving in hierarchical clausal specifications. SEKI-Report SR-95-14, FB Informatik, Universität Kaiserslautern, 1995.
J. A. Bergstra and J. W. Klop. Conditional rewrite rules: Confluence and termination. J. Computer and System Sci., 32:323–362, 1986.
A. Bouhoula and M. Rusinowitch. Implicit induction in conditional theories. J. Automated Reasoning, 14:189–235, 1995.
R. Boyer and J Moore. A Computational Logic. Academic Press, 1979.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, pages 243–320. Elsevier Science Publishers B. V., 1990.
N. Dershowitz, M. Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In 1st CTRS, volume 308 of LNCS, pages 31–44. Springer, 1988.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification. Springer, 1985.
D. Hutter and C. Sengler. INKA: The next generation. In 13th CADE, volume 1104 of LNAI, pages 288–292. Springer, 1996.
D. Kapur and M. Subramaniam. New uses of linear arithmetic in automated theorem proving by induction. J. Automated Reasoning, 16:39–78, 1996.
U. Kühler and C.-P. Wirth. Conditional equational specifications of data types with partial operations for inductive theorem proving. SEKI-Report SR-96-11, FB Informatik, Universität Kaiserslautern, 1996.
D. A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182–215, 1985.
M. Wirsing. Algebraic specification. In Handbook of Theoretical Computer Science, pages 675–788. Elsevier Science Publishers B. V., 1990.
C.-P. Wirth. Syntactic confluence criteria for positive/negative-conditional term rewriting systems. SEKI-Report SR-95-09, FB Informatik, Universität Kaiserslautern, 1995.
C.-P. Wirth and B. Gramlich, A constructor-based approach to positive/negative-conditional equational specifications. J. Symbolic Computation, 17:51–90, 1994.
C.-P. Wirth and B. Gramlich. On notions of inductive validity for first-order equational clauses. In 12th CADE, volume 814 of LNAI, pages 162–176. Springer, 1994.
C.-P. Wirth and U. Kühler. Inductive theorem proving in theories specified by positive/negative-conditional equations. SEKI-Report SR-95-15, FB Informatik, Universität Kaiserslautern, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kühler, U., Wirth, CP. (1997). Conditional equational specifications of data types with partial operations for inductive theorem proving. In: Comon, H. (eds) Rewriting Techniques and Applications. RTA 1997. Lecture Notes in Computer Science, vol 1232. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62950-5_60
Download citation
DOI: https://doi.org/10.1007/3-540-62950-5_60
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62950-4
Online ISBN: 978-3-540-69051-1
eBook Packages: Springer Book Archive