|
Browse All Reviews > Theory Of Computation (F) > Analysis Of Algorithms And Problem Complexity (F.2) > Nonnumerical Algorithms And Problems (F.2.2) > Complexity Of Proof Procedures (F.2.2...)
|
|
|
|
|
|
|
|
|
1-10 of 16
Reviews about "Complexity Of Proof Procedures (F.2.2...)":
|
Date Reviewed |
|
Circuit complexity, proof complexity, and polynomial identity testing: the ideal proof system Grochow J., Pitassi T. Journal of the ACM 65(6): 1-59, 2018. Type: Article
Cook and Reckhow [1] proved that NP ≠ coNP if and only if in every propositional proof system there is a tautology whose proof size has a super-polynomial lower bound (in terms of the size of the proved formula). Currently, i...
|
Feb 13 2019 |
|
The ordering principle in a fragment of approximate counting Atserias A., Thapen N. ACM Transactions on Computational Logic 15(4): 1-11, 2014. Type: Article
This paper solves an open problem in the field of bounded arithmetic. Bounded arithmetic is an area developed for the logical analysis of the expressive properties of the polynomial hierarchy in theoretical computer science [1]. Fragme...
|
Jan 27 2015 |
|
Formula caching in DPLL Beame P., Impagliazzo R., Pitassi T., Segerlind N. ACM Transactions on Computation Theory 1(3): 1-33, 2010. Type: Article
The DPLL algorithm is a satisfiability-based algorithm. The authors consider in this paper the extension of the DPLL approach to satisfiability checking, by adding memoization, which means saving previously solved subproblems for later...
|
Nov 30 2010 |
|
A stabilizer lemma for translation generalized quadrangles Thas K. European Journal of Combinatorics 28(1): 1-16, 2007. Type: Article
Generalized quadrangles are incidence structures introduced by J. Tits in his celebrated paper [1], as a means to study finite simple groups. Finite generalized quadrangles (GQs) embedded in a finite projective space are called finite ...
|
Jun 4 2007 |
|
On interactive proofs with a laconic prover Goldreich O., Vadhan S., Wigderson A. Computational Complexity 11(1/2): 1-53, 2003. Type: Article
As the authors state, “Interactive proof systems are two-party randomized protocols through which a computationally unbounded prover can convince a probabilistic polynomial-time verifier of the membership of a common input in...
|
Dec 21 2004 |
|
The complexity of PDL with interleaving Mayer A., Stockmeyer L. Theoretical Computer Science 161(1-2): 109-122, 1996. Type: Article
Previous work refining complexity measures for PDL with interleaving is extended in this paper. PDL is the propositional dynamic logic introduced by Fisher and Ladner in 1979. It uses the operator of union to express nondeterminacy. PD...
|
Mar 1 1997 |
|
Efficient checking of polynomials and proofs and the hardness of approximation problems Sudan M., Springer-Verlag, London, UK, 1995. Type: Book (9783540606154)
The computational intractability of NP-hard problems has occupied the minds of many computer theorists ever since Cook and Levin introduced them to computer science in the early 1970s. Karp’s subsequent formulation of a theor...
|
Nov 1 1996 |
|
A variational method for analysing unit clause search Méjean H., Morel H., Reynaud G. SIAM Journal on Computing 24(3): 621-649, 1995. Type: Article
The problem of testing whether a conjunctive normal form F is satisfiable is known as the satisfiability problem. When each clause has at most three literals, the problem is called 3-SAT. In this paper, the UC algori...
|
Aug 1 1996 |
|
A corrigendum for the optimized-IPIA Kean A., Tsiknis G. Journal of Symbolic Computation 17(2): 181-187, 1994. Type: Article
The main purpose of this paper is to correct an inaccurately reported algorithm. In 1990, the authors reported on an algorithm called IPIA, which incrementally generates the prime implicates/implicants of a set of clauses [1]. An impro...
|
Oct 1 1995 |
|
The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics Chen C., Lin I. Theoretical Computer Science 129(1): 95-121, 1994. Type: Article
In prior research with modal logic S5, restriction from general to Horn clause form yielded polynomial-time complexity for satisfiability, giving rise to hope that a similar situation might prevail for other modal logics. This paper&am...
|
Aug 1 1995 |
|
|
|
|
|
|