Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > SEQUENT CALCULUS:
Reports tagged with sequent calculus:
TR00-087 | 14th November 2000
Albert Atserias, Nicola Galesi, Pavel Pudlak

#### Monotone simulations of nonmonotone propositional proofs

We show that an LK proof of size \$m\$ of a monotone sequent (a sequent

that contains only formulas in the basis \$\wedge,\vee\$) can be turned

into a proof containing only monotone formulas of size \$m^{O(\log m)}\$

and with the number of proof lines polynomial in \$m\$. Also we show

... more >>>

TR13-016 | 17th January 2013
Olaf Beyersdorff

#### The Complexity of Theorem Proving in Autoepistemic Logic

Revisions: 1

Autoepistemic logic is one of the most successful formalisms for nonmonotonic reasoning. In this paper we provide a proof-theoretic analysis of sequent calculi for credulous and sceptical reasoning in propositional autoepistemic logic, introduced by Bonatti and Olivetti (ACM ToCL, 2002). We show that the calculus for credulous reasoning obeys almost ... more >>>

TR16-011 | 27th January 2016
Olaf Beyersdorff, Ján Pich

#### Understanding Gentzen and Frege systems for QBF

Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from Beyersdorff et al., denoted EF+\$\forall\$red, which is a ... more >>>

ISSN 1433-8092 | Imprint