Skip to main content
PRL Project

A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems

by Christoph Kreitz, Stephan Schmitt

Journal of Information and Computation.

  • unofficial copies PDF, PS

We present a uniform algorithm for transflorming machine-found matrix proofs in classiscal, constructive, and modal logics into sequent proofs. It is based on unified representations of matrix characterizations, of sequent calculi, and of prefixed sequent systems for various logics. The peculiarities of an individual logic are described by certain parameters of these representations, which are summarized in tables to be consulted by the conversion algorithm.

bibTex ref: KS00

cite link