Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > PROOF SYSTEMS:
Reports tagged with proof systems:
TR95-038 | 2nd July 1995
Joe Kilian, Erez Petrank

#### An Efficient Non-Interactive Zero-Knowledge Proof System for NP with General Assumptions

We consider noninteractive zero-knowledge proofs in the shared random
string model proposed by Blum, Feldman and Micali \cite{bfm}. Until
recently there was a sizable polynomial gap between the most
efficient noninteractive proofs for {\sf NP} based on general
complexity assumptions \cite{fls} versus those based on specific
algebraic assumptions \cite{Da}. ... more >>>

TR01-044 | 14th June 2001
Pavel Pudlak

#### On reducibility and symmetry of disjoint NP-pairs

We consider some problems about pairs of disjoint $NP$ sets.
The theory of these sets with a natural concept of reducibility
is, on the one hand, closely related to the theory of proof
systems for propositional calculus, and, on the other, it
resembles the theory of NP completeness. Furthermore, such
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 >>>

TR08-075 | 7th July 2008
Olaf Beyersdorff, Johannes Köbler, Sebastian Müller

#### Nondeterministic Instance Complexity and Proof Systems with Advice

Motivated by strong Karp-Lipton collapse results in bounded arithmetic, Cook and Krajicek have recently introduced the notion of propositional proof systems with advice.
In this paper we investigate the following question: Do there exist polynomially bounded proof systems with advice for arbitrary languages?
Depending on the complexity of the ... more >>>

TR11-110 | 10th August 2011
Alessandro Chiesa, Michael Forbes

#### Improved Soundness for QMA with Multiple Provers

Revisions: 1

We present three contributions to the understanding of QMA with multiple provers:

1) We give a tight soundness analysis of the protocol of [Blier and Tapp, ICQNM '09], yielding a soundness gap $\Omega(N^{-2})$, which is the best-known soundness gap for two-prover QMA protocols with logarithmic proof size. Maybe ... more >>>

TR12-079 | 14th June 2012
Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer

#### Verifying Proofs in Constant Depth

In this paper we initiate the study of proof systems where verification of proofs proceeds by NC0 circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages can be enumerated by NC0 functions. Our results show that the answer ... more >>>

TR12-164 | 17th November 2012
Rafail Ostrovsky, Ivan Visconti

#### Simultaneous Resettability from Collision Resistance

In FOCS 2001, Barak, Goldreich, Goldwasser and Lindell conjectured that the existence of ZAPs, introduced by Dwork and Naor in FOCS 2000, could lead to the design of a zero-knowledge proof system that is secure against both resetting provers and resetting verifiers. Their conjecture has been proven true by Deng, ... more >>>

TR12-186 | 27th December 2012
Andreas Krebs, Nutan Limaye

#### DLOGTIME-Proof Systems

We define DLOGTIME proof systems, DLTPS, which generalize NC0 proof systems.
It is known that functions such as Exact-k and Majority do not have NC0 proof systems. Here, we give a DLTPS for Exact-k (and therefore for Majority) and also for other natural functions such as Reach and k-Clique. Though ... more >>>

TR14-014 | 28th January 2014
Olaf Beyersdorff, Leroy Chew

#### The Complexity of Theorem Proving in Circumscription and Minimal Entailment

Circumscription is one of the main formalisms for non-monotonic reasoning. It uses reasoning with minimal models, the key idea being that minimal models have as few exceptions as possible. In this contribution we provide the first comprehensive proof-complexity analysis of different proof systems for propositional circumscription. In particular, we investigate ... more >>>

TR14-032 | 8th March 2014
Olaf Beyersdorff, Leroy Chew

#### Tableau vs. Sequent Calculi for Minimal Entailment

In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (J. Autom. Reasoning, 1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e., MLK p-simulates OTAB. The simulation is technically very involved ... more >>>

TR16-048 | 11th March 2016
Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda

#### Lifting QBF Resolution Calculi to DQBF

We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Resolution < IR-calc < IRM-calc, the ... more >>>

TR20-112 | 8th June 2020

#### Simulating DQBF Preprocessing Techniques with Resolution Asymmetric Tautologies

Dependency quantified Boolean formulas (DQBF) describe an NEXPTIME-complete generalisation of QBF, which in turn generalises SAT. QRAT is a recently proposed proof system for quantified Boolean formulas (QBF), which simulates the full suite of QBF preprocessing techniques and thus forms a uniform proof checking format for solver verification.

In this ... more >>>

TR21-068 | 8th May 2021
Marcel Dall'Agnol, Tom Gur, Subhayan Roy Moulik, Justin Thaler

#### Quantum Proofs of Proximity

We initiate the systematic study of QMA algorithms in the setting of property testing, to which we refer as QMA proofs of proximity (QMAPs). These are quantum query algorithms that receive explicit access to a sublinear-size untrusted proof and are required to accept inputs having a property $\Pi$ and reject ... more >>>

TR22-054 | 21st April 2022
Anastasia Sofronova, Dmitry Sokolov

#### A Lower Bound for $k$-DNF Resolution on Random CNF Formulas via Expansion

Random $\Delta$-CNF formulas are one of the few candidates that are expected to be hard to refute in any proof system. One of the frontiers in the direction of proving lower bounds on these formulas is the $k$-DNF Resolution proof system (aka $\mathrm{Res}(k)$). Assume we sample $m$ clauses over $n$ ... more >>>

ISSN 1433-8092 | Imprint