IANDC
2000
13 years 6 months ago
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 repre...
MLQ
2008
13 years 6 months ago
2008
We observe that removing contraction from a standard sequent calculus for first-order predicate logic preserves completeness for the modal fragment.
IGPL
2008
13 years 6 months ago
2008
In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: (i) given an unprovable sequent G, find a sentence H such ...
CSL
2003
Springer
14 years 18 hour ago
2003
Springer
System SKS is a set of rules for classical propositional logic presented in the calculus of structures. Like sequent systems and unlike natural deduction systems, it has an explici...
PADL
2004
Springer
14 years 4 days ago
2004
Springer
Gentzen’s Hauptsatz – cut elimination theorem – in sequent calculi reveals a fundamental property on logic connectives in various logics such as classical logic and intuition...
WOLLIC
2009
Springer
14 years 1 months ago
2009
Springer
Bi-intuitionistic logic is the extension of intuitionistic logic with exclusion, a connective dual to implication. Cut-elimination in biintuitionistic logic is complicated due to t...