Unsolvable systems of equations and proof complexity

DOI10.4171/DMS/1-3/44MaRDI QIDQ1126839zbMATH OpenFDO

Authors Toniann Pitassi

Publication date 5 August 1998

Published in Documenta Mathematica (Search for Journal in Brave)

Full work available at URL https://eudml.org/doc/232165, http://www.emis.de/journals/DMJDMV/xvol-icm/14/Pitassi.MAN.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

algebraic approach to the efficiency of propositional proof systemspropositional proof complexitysurveysystem of equations

Mathematics Subject Classification ID

Classical propositional logic (03B05) Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25)

Review text

This is a survey of an algebraic approach to the efficiency of propositional proof systems. To a formula \(C\) in conjunctive normal form, one associates a set of polynomials \(Q_i\). (An atom \(p\) goes to \(1-y\), \(\neg p\) to \(y\), and \(\vee\) is replaced by \(x\). Thus each conjunct results in a polynomial. And, add \(y^2-y\) to confine the values to \(0\) and \(1\).) The given \(C\) is refutable iff the \(Q_i\)'s have no \(0/1\) solution iff, by the Nullstellensatz, \(\sum P_iQ_i= 1\) for some \(P_i\)'s. According to the author, ``Algebraic proof systems are appealing because of their simplicity and non-syntactic nature -- and, of course, much work has been done by algebraists on equations, the Nullstellensatz, etc. She compares algebraic proofs to Frege, resolution systems, etc., and talks about some methods and results (e.g., the design method, lower bounds for pigeonhole principles). The author gives good directions for future work by citing and commenting on open problems. We have also a recent good survey article by \textit{A. Urquhart} about ``The complexity of propositional proofs [Bull. Symb. Log. 1, No. 4, 425-467 (1995; Zbl 0845.03025)]. Compared to it, the present article is more research oriented in a narrowly focused area.

Recommendations

• scientific article; zbMATH DE number 1059248
• Proof theory
• scientific article; zbMATH DE number 1860672
• Complexity of propositional proofs (invited talk)
• Algebraic proof systems over formulas.
• scientific article; zbMATH DE number 3976991
• Counting proofs in propositional logic
• Usablity of some theorem proving systems
• scientific article; zbMATH DE number 475244
• Polynomial size proofs of the propositional pigeonhole principle

Cited in

(6)

• Algebraic proof systems over formulas.
• On the Complexity of Hmelevskii’s Theorem and Satisfiability of Three Unknown Equations
• scientific article; zbMATH DE number 1059248 (Why is no real title available?)
• Characterizing propositional proofs as noncommutative formulas
• Semialgebraic proofs, IPS lower bounds, and the -conjecture: can a natural number be negative?
• A lower bound for polynomial calculus with extension rule

This page was built for publication: Unsolvable systems of equations and proof complexity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1126839)