Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Session 6A

Converting non-classical matrix proofs into sequent-style systems

Stephan SchmittContact Information and Christoph KreitzContact Information

(1)  FG Intellektik, FB Informatik, TH Darmstadt, Alexanderstr. 10, 64283 Darmstadt, Germany
Abstract
We present a uniform algorithm fot transforming matrix proofs in classical, constructive, and modal logics into sequent style proofs. Making use of a similarity between matrix methods and Fitting's prefixed tableaus we first develop a procedure for extracting a prefixed sequent proof from a given matrix proof. By considering the additional restrictions on the order of rule applications we then extend this procedure into an algorithm which generates a conventional sequent proof.
Our algorithm is based on unified representations of matrix characterizations for various logics as well as of prefixed and usual sequent calculi. The peculiarities of a logic are encoded by certain parameters which are summarized in tables to be consulted by the algorithm.
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.113 • Server: MPWEB26
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)