Abstract
In this paper we are interested in an algebraic specification language that (1) allows for sufficient expessiveness, (2) admits a well-defined se-mantics, and (3) allows for formal proofs. To that end we study clausal specifications over built-in algebras. To keep things simple, we consider built-in algebras only that are given as the initial model of a Horn clause specification. On top of this Horn clause specification new operators are (partially) defined by positive/negative conditional equations. In the first part of the paper we define three types of semantics for such a hierarchical specification: model-theoretic, operational, and rewrite-based semantics. We show that all these semantics coincide, provided some restrictions are met. We associate a distinguished algebra A spec to a hierachical specification spec. This algebra is initial in the class of all models of spec. In the second part of the paper we study how to prove a theorem (a clause) valid in the distinguished algebra A spec. We first present an abstract framework for inductive theorem provers. Then we instantiate this framework for proving inductive validity., Finally we give some examples to show how concrete proofs are carried out.
This report was supported by the Deutsche Forschungsgemeinchaft, SFB 314 (D4-Projekt)
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J. Avenhaus. Reduktionssysteme (in German), Springer-Verlag, 1995
J. Avenhaus, K. Becker. Operational specifications with built-ins., In Proc. 11th Annual Symposium on Theoretical Aspects of Computer Science, volume 775 of Lecture Notes in Computer Science, pages 263–274. Springer-Verlag, 1994.
J. Avenhaus and C. Loría-Sáenz., On conditional rewrite systems with extra variables and deterministic logic programs. In Proc. Int. Conference on Logic Programming and Automated Reasoning, volume 822 of Lecture Notes in Computer Science, pages 215–229. Springer-Verlag, 1994
L. Bachmair. Proof by consistency in equational theories., In Proc. 3 rd Annual IEEE Symposium on Logic in Computer Science, pages 228–233, 1988.
L. Bachmair, H. Ganzinger. Rewrite-based equational teorem proving with selection and simplification., J. Logic and Computation, 4 (3): 1–31, 1994.
K. Becker. Rewrite operationalization of clausal specifications with predefined structures. PhD thesis, Univ. Kaiserslautern, 1994
E. Bevers, J. Lewi. Proof by consistency in conditional equaltional theories., In Proc. 2 nd International Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, pages 194–205. Springer-Verlag, 1990
A. Bouhoula, M. Rusinowitch. Automatic case analysis in proof by induction., In Proc. of the 13 th IJCAI, pages 88–94, 1993.
RR. Boyer, JS. Moore., A Computational Logic, Academic Press, 1979.
M. Broy, M. Wirsing, C. Pair. A systematic study of models of abstract data types., Theoretical Computer Science, pages 139–174, 1984.
N. Dershowitz, J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243-320. Elsevier, 1990
B. Gramlich. Completion based inductive theorem proving: A case study in verifying sorting algorithms. SEKI-Report SR-90-04, Fachbereich Infor-matik, Universität Kaiserslautern, 1990
G.P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, pages 797–821, 1980.
G.P. Huet, J.-M., Hullot., Proofs by induction in equational theories with constructors., Journal of Computer and System Sciences, 25: 239–266, 1982.
J.-P. Jouannaud and E. Kounalis., Automatic proofs by induction in theories without constructors., Information and Computation, 82: 1–33, 1989.
S. Kaplan. Conditional rewrite rules., Theoretical Computer Science, 33: 175–193, 1984.
S. Kaplan. Positive/negative conditional rewriting., In Proc. 1 st International Workshop on Conditional Term Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 129–143. Springer-Verlag, 1988
D. Kapur and D. Musser. Proof by consistency., Artificial Intelligence, 31: 125–157, 1987.
D. Kapur and D.R. Musser. Inductive reasoning with incomplete specifications., In Proc. 1 st Annual IEEE Symposium on Logic in Computer Science, pages 367–377. IEEE Computer Society Press, 1986.
P. Padawitz. Deduction and declarative programming, Cambridge University Press, 1992.
U.S. Reddy. Term rewriting induction., In Proc. 10 th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 162–177. Springer-Verlag, 1990
Chr. Walther. Mathematical induction,. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2. Oxford University Press, 1994
W. Wechler. Universal algebra for computer scientists, volume 25 of EATCS Monographs on Theoretical Computer Sciences, Springer-Verlag, 1992
C.-P. Wirth. Syntactic confluence criteria for positive/negative-conditional term rewriting systems. SEKI-Report SR-95-09, Fachbereich Informatik, Universität Kaiserslautern, 1995
C.-P. Wirth. Positive/negative-conditional equations: A constructor based framework for specification and inductive theorem proving. PhD thesis, Univ. Kaiserslautern, 1996
C.-P. Wirth and K. Becker., Abstract notions and inference systems for proofs by mathematical induction., In Proc. 4th International Workshop on Conditional and Typed Rewriting Systems, volume 968 of Lecture Notes in Computer Science, pages 353–373. Springer-Verlag, 1994
C.-P. Wirth and B. Gramlich., A constructor-based approach for positive/negative conditional equational specifications., In Proc. 3rd International Workshop on Conditional Term Rewriting Systems, volume 656 of Lecture Notes in Computer Science, pages 198–212. Springer-Verlag, 1993
C.-P. Wirth and B. Gramlich., A constructor-based approach to positive/negative-conditional equational specifications., Journal of Symbolic Computation, 17: 51–90, 1994.
C.-P. Wirth and B. Gramlich., On notions of inductive validity for first- order equational clauses. In Proc. 12 th International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 162–176. Springer-Verlag, June 1994.
H. Zhang, D. Kapur, and M.S. Krishnamoorthy., A mechanizable induction principle for equational specifications., In Proc. 9 th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 162–181. Springer-Verlag, 1988
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Kluwer Academic Publishers
About this chapter
Cite this chapter
Avenhaus, J., Madlener, K. (1997). Theorem Proving in Hierarchical Clausal Specifications. In: Du, DZ., Ko, KI. (eds) Advances in Algorithms, Languages, and Complexity. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-3394-4_1
Download citation
DOI: https://doi.org/10.1007/978-1-4613-3394-4_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-3396-8
Online ISBN: 978-1-4613-3394-4
eBook Packages: Springer Book Archive