Abstract
Formal methods for program verification, optimization, and synthesis rely on complex mathematical proofs, which often involve reasoning about computations. Because of that there is no single automated proof procedure that can handle all the reasoning problems occurring during a program derivation or verification. Instead, one usually relies on proof assistants like NuPRL (Constable et al., 1986), Coq (Dowek and et. al, 1991), Alf (Altenkirch et al., 1994) etc., which are based on very expressive logical calculi and support interactive and tactic controlled proof and program development. Proof assistants, however, suffer from a very low degree of automation, since all their inferences must eventually be based on sequent or natural deduction rules. Even proof parts that rely entirely on predicate logic can seldomly be found automatically, as there are no complete proof search procedures embedded into these systems. It is therefore desirable to extend the reasoning power of proof assistants by integrating well-understood techniques from automated theorem proving.
This is a preview of subscription content, log in via an institution to check access.
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
Altenkirch, T., Gaspes, V., Nordström, B., and von Sydow, B. (1994). A user’s guide to ALF. University of Göteborg.
Bates, J. L. and Constable, R. L. (1985). Proofs as programs. ACM Transactions on Programming Languages and Systems, 7 (1): 113–136.
Bibel, W. (1981). On matrices with connections. Journal of the ACM, 28: 633–645.
Bibel, W. (1987). Automated Theorem Proving. Vieweg Verlag, second edition.
Bibel, W. (1992). Deduktion —Automatisierung der Logik. Oldenbourg.
Bibel, W., Korn, D., Kreitz, C., and Schmitt, S. (1996). Problem-oriented applications of automated theorem proving. In Carnet, J. and Limongelli, C., editors, Design and Implementation of Symbolic Computation Systems, LNCS 1126, pages 1–21.
Bibel, W., Korn, D., Kreitz, C., Kurucz, F., Otten, J., Schmitt, S., and Stolpmann, G. (1998). A multi-level approach to program synthesis. In Fuchs, N., editor, Seventh International Workshop on Logic Program Synthesis and Transformation (LOPSTR’97), LNAI 1463, pages 1–25.
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., and Smaill, A. (1993). Rippling: a heuristic for guiding inductive proofs. Artificial Intelligence, 62 (2): 185–253.
Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendier, N. P., Panangaden, P., Sasaki, J. T., and Smith, S. F. (1986). Implementing Mathematics with the NuPRL proof development system. Prentice Hall.
Dowek, G. and et. al (1991). The Coq proof assistant user’s guide. Institut National de Recherche en Informatique et en Automatique. Report RR 134.
Kreitz, C. (1996). Formal mathematics for verifiably correct program synthesis. Journal of the IGPL, 4 (1): 75–94.
Kreitz, C., Otten, J., and Schmitt, S. (1996). Guiding Program Development Systems by a Connection Based Proof Strategy. In Proietti, M., editor, Proceedings of the Fifth International Workshop on Logic Program Synthesis and Transformation,LNCS 1048, pages 137–151. Springer Verlag.
Kreitz, C., Mantel, H., Otten, J., and Schmitt, S. (1997). Connection-Based Proof Construction in Linear Logic. In McCune, W., editor, Proceedings of the 14 th Conference on Automated Deduction,LNAI 1249, pages 207–221. Springer Verlag.
Kreitz, C. (1998). Program synthesis. In Bibel, W. and Schmitt, P., editors, Automated Deduction — A Basis for Applications,chapter III.2.5, pages 105–134. Kluwer.
Kreitz, C., Hayden, M., and Hickey, J. (1998). A proof environment for the development of group communication systems. In Kirchner, C. and Kirchner. H., editors, 15 th International Conference on Automated Deduction,LNAI 1421, pages 317–332. Springer Verlag.
Kreitz, C. and Otten, J. (1999). Connection-based Theorem Proving in Classical and Non-classical Logics. Journal for Universal Computer Science, 5 (3): 88–112.
Kurucz, F. (1997). Realisierung verschiedender Induktionsstrategien basierend auf dem Rippling-Kalkül. Diplomarbeit, Darmstadt University of Technology.
Mantel, H. and Kreitz, C. (1998). A matrix characterization for MELL. 6th European Workshop on Logics in Artificial Intelligence, European Workshop, JELIA ’88, LNAI 1489, pages 169–183, Springer Verlag.
Otten, J. and Kreitz, C. (1995). A connection based proof method for intuitionistic logic. In Baumgartner, P., Hähnle, R., and Posegga, J., editors, Proceedings of the 4 t h Workshop on Theorem Proving with Analytic Tableaux and Related Methods,LNAI 918, pages 122–137. Springer Verlag.
Otten, J. and Kreitz, C. (1996). T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. In Moscato, U., editor, Proceedings of the 5t h Workshop on Theorem Proving with Analytic Tableaux and Related Methods,LNAI 1071, pages 244–260. Springer Verlag.
Pientka, B. and Kreitz, C. (1998). Instantiation of existentially quantified variables in inductive specification proofs. In 4th International Conference on Artificial Intelligence and Symbolic Computation,LNAI 1476, pages 247–258. Springer Verlag.
Schmitt, S. and Kreitz, C. (1995). On transforming intuitionistic matrix proofs into standard-sequent proofs. In Baumgartner, P., Hähnle, R., and Posegga, J., editors, Proceedings of the 4t h Workshop on Theorem Proving with Analytic Tableaux and Related Methods,LNAI 918, Springer Verlag.
Schmitt, S. and Kreitz, C. (1996). Converting non-classical matrix proofs into sequent-style systems. In McRobbie, M. and Slaney, J., editors, Proceedings of the 13 th Conference on Automated Deduction,LNAI 1104, pages 418–432. Springer Verlag.
Schmitt, S. and Kreitz, C. (1998). Deleting redundancy in proof reconstruction. In de Swaart, H., editor, International Conference TABLEAUX-98,LNAI 1397, pages 262–276. Springer Verlag.
Wallen, L. (1990). Automated deduction in nonclassical logic. MIT Press.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Kreitz, C., Otten, J., Schmitt, S., Pientka, B. (2000). Matrix-Based Constructive Theorem Proving. In: Hölldobler, S. (eds) Intellectics and Computational Logic. Applied Logic Series, vol 19. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9383-0_12
Download citation
DOI: https://doi.org/10.1007/978-94-015-9383-0_12
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5438-8
Online ISBN: 978-94-015-9383-0
eBook Packages: Springer Book Archive