Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > FREGE SYSTEMS:
Reports tagged with Frege systems:
TR01-011 | 21st January 2001
Dima Grigoriev, Edward Hirsch

#### Algebraic proof systems over formulas

We introduce two algebraic propositional proof systems F-NS
and F-PC. The main difference of our systems from (customary)
Nullstellensatz and Polynomial Calculus is that the polynomials
are represented as arbitrary formulas (rather than sums of
monomials). Short proofs of Tseitin's tautologies in the
constant-depth version of F-NS provide ... more >>>

TR07-032 | 27th March 2007
Pavel Pudlak

#### Quantum deduction rules

We define propositional quantum Frege proof systems and compare it
with classical Frege proof systems.

more >>>

TR11-174 | 30th December 2011
Pavel Hrubes, Iddo Tzameret

#### Short Proofs for the Determinant Identities

Revisions: 1

We study arithmetic proof systems \$\mathbb{P}_c(\mathbb{F})\$ and \$\mathbb{P}_f(\mathbb{F})\$ operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field \$\mathbb{F}\$. We establish a series of structural theorems about these proof systems, the main one stating that \$\mathbb{P}_c(\mathbb{F})\$ proofs can be balanced: if a polynomial identity of ... more >>>

TR12-018 | 24th February 2012
Joerg Flum, Moritz Müller

#### Some definitorial suggestions for parameterized proof complexity

We introduce a (new) notion of parameterized proof system. For parameterized versions of standard proof systems such as Extended Frege and Substitution Frege we compare their complexity with respect to parameterized simulations.

more >>>

TR15-133 | 12th August 2015
Olaf Beyersdorff, Ilario Bonacina, Leroy Chew

#### Lower bounds: from circuits to QBF proof systems

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from ... 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 >>>

TR18-178 | 9th October 2018
Leroy Chew

#### Hardness and Optimality in QBF Proof Systems Modulo NP

Quantified Boolean Formulas (QBFs) extend propositional formulas with Boolean quantifiers. Working with QBF differs from propositional logic in its quantifier handling, but as propositional satisfiability (SAT) is a subproblem of QBF, all SAT hardness in solving and proof complexity transfers to QBF. This makes it difficult to analyse efforts dealing ... more >>>

TR21-021 | 18th February 2021
Per Austrin, Kilian Risse

#### Average-Case Perfect Matching Lower Bounds from Hardness of Tseitin Formulas

We study the complexity of proving that a sparse random regular graph on an odd number of vertices does not have a perfect matching, and related problems involving each vertex being matched some pre-specified number of times. We show that this requires proofs of degree \$\Omega(n/\log n)\$ in the Polynomial ... more >>>

ISSN 1433-8092 | Imprint