A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems
Christoph Kreitz, Stephan Schmitt.
Journal of Information and Computation 162(1-2):226-254, 2000.
Abstract
	We present a uniform algorithm for transforming machine-found matrix proofs in classical, 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.

		(Preprint)	Back to overview of papers
Bibtex Entry
	@Article{ar:KreitzSchmitt00a, author = "Christoph Kreitz and Stephan Schmitt", title = "A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems", journal = "Journal of Information and Computation", year = "2000", volume = "162", number = "1--2", pages = "226--254", }