Abstract
We present a method for automated theorem proving in a combination of theories with disjoint signatures. The Nelson-Oppen combination technique for decision procedures is used to combine separate theorem provers in different theories. The provers being combined are based on the Prolog Technology Theorem Proving method and they use the SLD resolution (alternatively Model Elimination) as an inference system. Our approach enables to tune up the provers for different theories separately and increases the effciency of automated theorem proving in a combination of theories.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Apt K.R, Introduction to Logic Programming (Revised and Extended Version), Report CS-R8826, Centre for Math. and Comp. Science, 1986 Amsterdam
Baader F., Tinelli C.: A New Approach for Combining Decision Procedures for the Word Problem and Its Connection to the Nelson-Oppen Combination method, pg. 19–33in proc. CADE-14, LNAI 1249, ed. W. McCune, Springer 1997
Baumgartner P., Furbach U.: Model Elimination Without Contrapositives and its Application to PTTP, in Proc. CADE-14, LNAI 1249, ed. W. McCune, Springer 1997
Bjorner N.S., Stickel M.E., Uribe, T.E.: A Practical Integration of First-Order Reasoning and Decision procedures, pg. 101–115 in proc. CADE-14, LNAI 1249, ed. W. McCune, Springer 1997
Boulton R.J.: Combining Decision Procedures in the HOL system, pg. 75–89, LNCS 971, Higher Order Logic Theorem Proving and Its Applications, 1995
Burstall R.M, Sanella D.T.: Structured theories in LCF, Proceedings of the 8th Colloquium on Trees in Algebra and Programming, L’Aquila, Italy, 1983
Busch H.: First-Order Automation for Higher-Order-Logic Theorem Proving, pg. 97–112, LNCS 859, Higher Order Logic Theorem Proving and Its Applications 1994
Chang C.L., Lee R.C.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973
Dahn B.I., Gehne J., Honigmann Th., Wolf A.: Integration of Automated and Interactive Theorem Proving in ILF, pg. 57–60 in proc. CADE-14, LNAI 1249, ed. W. McCune, Springer 1997
Harper R., Sanella D., Tarlecki A.: Structured theory presentations and logic representations, p. 113–160, Annals of pure and Applied Logic, North Holland 1994
Harrison J.: First Order Logic in Practice, Proceedings of FTP97 Workshop, 1997, RISC report No 97-50
Nelson G., Oppen C.: Simplification by cooperating Decision Procedures, pg. 245–257, ACM Transactions on Programming Languages and Systems, 1/2, 1979
Nilsson N.J.: Principles of Artificial Intelligence, Tioga Publishing Co., Palo Alto, California (1980), 193–275
Plaisted D.A.: Non-Horn Clause Logic Programming Without Contrapositives, pg. 287–325, Journal of Automated Reasoning 4(1988)
Reif W., Schellhorn G.: Proving properties of Finite Enumerations: A Problem Set for Automated Theorem Provers, Technical Report Nr. 97-12, Department of Computer Science, University of Ulm
Reif W., Schellhorn G.: Theorem Proving in Large Theories, Proceedings of FTP97 Workshop, 1997, RISC report No 97-50
Shostak, R.E.: Deciding combinations of theories, LNCS 138, 6th Conference on Automated Deduction, (CADE 6), LNCS 138, ed. D.W. Loveland, Springer 1982
Stickel M.E.: A Prolog technology theorem prover: a new exposition and implementation in Prolog, pg. 109–128, Theoretical Computer Science 104 (1992)
Stickel M.E.: A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler, pg. 353–380, Journal of Automated Reasoning 4 (1988)
Tinelli. C., Harandi. M.: A new correctness proof of the Nelson-Oppen combination procedure, proc. of the 1st International Workshop Frontiers of Combining Systems, 1996
Vanousek P.: Implication based theorem proving (in Czech), Diploma Thesis, MFF Charles University Prague, 1995
Vanousek P.: Automated Theorem Proving in Structured Theory Specifications (Choosing implementional environment), Tech rep. 98-03, MFF Charles University Prague, 1998
Vanousek P.: Automated Theorem Proving in Structured Theory Specifications, Dissertation Thesis (in progress), MFF Charles University Parague, 1998
Wirsing M., Proofs In Structured Specifications, MIP-9008, 1991 University Passau
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Anousek, P. (1998). Automated Theorem Proving in a Combination of Theories with Disjoint Signatures. In: Rovan, B. (eds) SOFSEM’ 98: Theory and Practice of Informatics. SOFSEM 1998. Lecture Notes in Computer Science, vol 1521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49477-4_37
Download citation
DOI: https://doi.org/10.1007/3-540-49477-4_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65260-1
Online ISBN: 978-3-540-49477-5
eBook Packages: Springer Book Archive