Deleting Redundancy in Proof Reconstruction

  • Stephan Schmitt
  • Christoph Kreitz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


We present a framework for eliminating redundancies during the reconstruction of sequent proofs from matrix proofs. We show that search-free proof reconstruction requires knowledge from the proof search process. We relate different levels of proof knowledge to reconstruction knowledge and analyze which redundancies can be deleted by using such knowledge. Our framework is uniformly applicable to classical logic and all non-classical logics which have a matrix characterization of validity and enables us to build adequate conversion procedures for each logic.


Intuitionistic Logic Decomposition Problem Sequent Rule Proof Search Logical Validity 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    W. Bibel. On matrices with connections. Journal of the ACM, 28, p. 633–645, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    W. Bibel. Automated theorem proving. Vieweg, 1987.Google Scholar
  3. 3.
    W. Bibel, S. Brüning, U. Egly, T. Rath. Komet. CADE-12, LNAI 814, pp. 783–787. 1994.Google Scholar
  4. 4.
    W. Bibel, D. Korn, C. Kreitz, F. Kurucz, J. Otten, S. Schmitt, G. Stolpmann. A Multi-Level Approach to Program Synthesis. 7thLOPSTR Workshop, LNCS, 1998.Google Scholar
  5. 5.
    W. Bibel, D. Korn, C. Kreitz, S. Schmitt. Problem-Oriented Applications of Automated Theorem Proving. DISCO-96, LNCS 1128, pp. 1–21, 1996.Google Scholar
  6. 6.
    M. C. Fitting. Proof Methods for Modal and Intuitionistic Logic. D. Reidel, 1983.Google Scholar
  7. 7.
    C. Kreitz, H. Mantel, J. Otten, S. Schmitt. Connection-based proof construction in Linear Logic. CADE-14, 1997.Google Scholar
  8. 8.
    C. Kreitz, J. Otten, and S. Schmitt. Guiding Program Development Systems by a Connection Based Proof Strategy. 5thLOPSTR Workshop, LNCS 1048, pp. 137–151. 1996.Google Scholar
  9. 9.
    R. Letz, J. Schumann, S. Bayerl, W. Bibel. Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    H. J. Ohlbach. A resolution calculus for modal logics. PhD Thesis, Univ. Kaiserslautern, 1988.Google Scholar
  11. 11.
    J. Otten, C. Kreitz. T-string-unification: unifying prefixes in non-classical proof methods. 5thTABLEAUX Workshop, LNAI 1071, pp. 244–260, 1996.Google Scholar
  12. 12.
    J. Otten, C. Kreitz. A uniform proof procedure for classical and non-classical logics. KI-96: Advances in Artificial Intelligence, LNAI 1137, pp. 307–319, 1996.Google Scholar
  13. 13.
    J. Otten. ileanTAP: An intuitionistic theorem prover. 6thTABLEAUX Workshop, 1997.Google Scholar
  14. 14.
    J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.zbMATHCrossRefGoogle Scholar
  15. 15.
    S. Schmitt. Avoiding Redundnacy for Proof Reconstruction in Classical and Non-Classical Logics. Technical Report, TU-Darmstadt, 1997.Google Scholar
  16. 16.
    S. Schmitt, C. Kreitz. On transforming intuitionistic matrix proofs into standard-sequent proofs. 4thTABLEAUX Workshop, LNAI 918, pp. 106–121, 1995.Google Scholar
  17. 17.
    S. Schmitt, C. Kreitz. Converting non-classical matrix proofs into sequent-style systems. CADE-13, LNAI 1104, pp. 418–432, 1996.Google Scholar
  18. 18.
    S. Schmitt, C. Kreitz. A uniform procedure for converting non-classical matrix proofs into sequent-style systems. Technical Report AIDA-96-01, TU-Darmstadt, 1996.Google Scholar
  19. 19.
    T. Tammet A Resolution Theorem Prover for Intuitionistic Logic CADE-13, LNAI 1104, pp. 2–16, 1996.Google Scholar
  20. 20.
    L. Wallen. Matrix proof methods for modal logics. IJCAI-87, p. 917–923. 1987.Google Scholar
  21. 21.
    L. Wallen. Automated deduction in non-classical logics. MIT Press, 1990.Google Scholar
  22. 22.
    L. Wos et. al. Automated reasoning contributes to mathematics and logic. CADE-10, LNCS 449, p. 485–499. 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Stephan Schmitt
    • 1
  • Christoph Kreitz
    • 2
  1. 1.Fachgebiet Intellektik, Fachbereich InformatikDarmstadt University of TechnologyDarmstadtGermany
  2. 2.Department of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations