Proof reconstruction in classical and nonclassical logics (Diss., TU Darmstadt, 1999) (Q2726302)

This thesis develops uniform algorithms for proof transformation from proof calculi based on {matrix characterizations}, originally introduced by Prawitz (see \textit{P. B. Andrews} [J. Assoc. Comput. Mach. 28, 193-214 (1981; Zbl 0456.68119)], \textit{W. Bibel} [Automated theorem proving (1987; Zbl 0639.68092)], and \textit{L. A. Wallen} [Automated proof search in non-classical logics (1990; Zbl 0782.03003)]) to sequent calculi for various classical and nonclassical (modal, intuitionistic, linear) first-order logis. The idea is to transform machine-generated proofs (produced by automated theorem provers) into ones which can be comprehended and analyzed by mathematicians and programmers. NEWLINENEWLINENEWLINETwo basic design principles have been followed in the development of proof reconstruction algorithms: uniformity, i.e. the algorithms consist of an invariant part, common for all logics treated, and a variant part, specific for each source logic and target calculus; and {search-freeness} of the algorithms: no additional search should be involved in the reconstruction process. NEWLINENEWLINENEWLINEThe content of the thesis briefly: Chapter 1 introduces the target (sequent-based) and source (matrix-based) proof calculi for the modal and intuitionistic logics, and the multiplicative fragment MLL of linear logic, which will be treated further. Chapter 2 discusses the theoretical basics of proof reconstruction. Chapter 3 presents uniform algorithms for proof transformation from matrix proofs to sequent calculi for these logical systems. Chapter 4 develops search-free proof reconstruction algorithms. The last chapter summarizes the main contributions and discusses future research perspectives and applications.