Minimum propositional proof length is NP-hard to linearly approximate

Michael Alekhnovich; Sam Buss; Shlomo Moran; Toniann Pitassi

doi:10.2307/2694916

Minimum propositional proof length is NP-hard to linearly approximate

Journal of Symbolic Logic ◽

10.2307/2694916 ◽

2001 ◽

Vol 66 (1) ◽

pp. 171-191 ◽

Cited By ~ 17

Author(s):

Michael Alekhnovich ◽

Sam Buss ◽

Shlomo Moran ◽

Toniann Pitassi

Keyword(s):

Assignment Problem ◽

Sequent Calculus ◽

Hardness Of Approximation ◽

Np Hard ◽

Satisfying Assignment ◽

Proof Systems ◽

Frege Systems ◽

Propositional Proof ◽

Almost All ◽

Polynomial Calculus

AbstractWe prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution. Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

Download Full-text

ON NON-MONOTONOUS PROPERTIES OF SOME CLASSICAL AND NONCLASSICAL PROPOSITIONAL PROOF SYSTEMS

Proceedings of the YSU A: Physical and Mathematical Sciences ◽

10.46991/pysu:a/2020.54.3.127 ◽

2020 ◽

Vol 54 (3 (253)) ◽

pp. 127-136

Author(s):

Anahit A. Chubaryan ◽

Arsen A. Hambardzumyan

Keyword(s):

Cut Rule ◽

Proof Systems ◽

Nonclassical Logics ◽

Frege Systems ◽

Sequent Systems ◽

Propositional Proof Systems ◽

Propositional Proof

We investigate the relations between the proof lines of non-minimal tautologies and its minimal tautologies for the Frege systems, the sequent systems with cut rule and the systems of natural deductions of classical and nonclassical logics. We show that for these systems there are sequences of tautologies ψn, every one of which has unique minimal tautologies φn such that for each n the minimal proof lines of φn are an order more than the minimal proof lines of ψn.

Download Full-text

THE INFORMATIONAL CONTENT OF CANONICAL DISJOINT NP-PAIRS

International Journal of Foundations of Computer Science ◽

10.1142/s012905410900670x ◽

2009 ◽

Vol 20 (03) ◽

pp. 501-522 ◽

Cited By ~ 2

Author(s):

CHRISTIAN GLAßER ◽

ALAN L. SELMAN ◽

LIYU ZHANG

Keyword(s):

Open Problem ◽

Structural Complexity ◽

Informational Content ◽

Proof Systems ◽

Canonical Pair ◽

Propositional Proof Systems ◽

Np Complete ◽

Complete Sets ◽

Propositional Proof ◽

Almost All

We investigate the connection between propositional proof systems and their canonical pairs. It is known that simulations between propositional proof systems translate to reductions between their canonical pairs. We focus on the opposite direction and study the following questions. Q1: For which propositional proof systems f and g does the implication [Formula: see text] hold, and for which does it fail? Q2: For which propositional proof systems of different strengths are the canonical pairs equivalent? Q3: What do (non-)equivalent canonical pairs tell about the corresponding propositional proof systems? Q4: Is every NP-pair (A, B), where A is NP-complete, strongly many-one equivalent to the canonical pair of some propositional proof system? In short, we show that Q1 and Q2 can be answered with 'for almost all', which generalizes previous results by Pudlák and Beyersdorff. Regarding Q3, inequivalent canonical pairs tell that the propositional proof systems are not "very similar," while equivalent, P -inseparable canonical pairs tell that they are not "very different." We can relate Q4 to the open problem in structural complexity that asks whether unions of disjoint NP-complete sets are NP-complete. This demonstrates a new connection between propositional proof systems, disjoint NP-pairs, and unions of disjoint NP-complete sets.

Download Full-text

The deduction rule and linear and near-linear proof simulations

Journal of Symbolic Logic ◽

10.2307/2275228 ◽

1993 ◽

Vol 58 (2) ◽

pp. 688-709 ◽

Cited By ~ 15

Author(s):

Maria Luisa Bonet ◽

Samuel R. Buss

Keyword(s):

Propositional Logic ◽

Natural Deduction ◽

Sequent Calculus ◽

Upper Bounds ◽

Proof System ◽

Proof Systems ◽

Linear Speedup ◽

Frege Systems ◽

Deduction Rule ◽

Gentzen Sequent Calculus

AbstractWe introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof.A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by “nearly linear” is meant the ratio of proof lengths is O(α(n)) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O(n . α(n)). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O(n log n) lines and of height O(log n). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O(n log n).

Download Full-text

Chapter 7. Proof Complexity and SAT Solving

Frontiers in Artificial Intelligence and Applications - Handbook of Satisfiability ◽

10.3233/faia200990 ◽

2021 ◽

Author(s):

Sam Buss ◽

Jakob Nordström

Keyword(s):

Linear Algebra ◽

Cutting Planes ◽

Proof Complexity ◽

Sat Solving ◽

Proof Systems ◽

Frege Systems ◽

Ample Supply ◽

Clause Learning ◽

Algebraic Approaches ◽

Polynomial Calculus

This chapter gives an overview of proof complexity and connections to SAT solving, focusing on proof systems such as resolution, Nullstellensatz, polynomial calculus, and cutting planes (corresponding to conflict-driven clause learning, algebraic approaches using linear algebra or Gröbner bases, and pseudo-Boolean solving, respectively). There is also a discussion of extended resolution (which is closely related to DRAT proof logging) and Frege and extended Frege systems more generally. An ample supply of references for further reading is provided, including for some topics omitted in this chapter.

Download Full-text

Disjoint NP-Pairs and Propositional Proof Systems

ACM SIGACT News ◽

10.1145/2696081.2696095 ◽

2014 ◽

Vol 45 (4) ◽

pp. 59-75 ◽

Cited By ~ 1

Author(s):

C. Glaßer ◽

A. Hughes ◽

A. L. Selman ◽

N. Wisiol

Keyword(s):

Proof Systems ◽

Propositional Proof Systems ◽

Propositional Proof

Download Full-text

The Method of Socratic Proofs Meets Correspondence Analysis

Bulletin of the Section of Logic ◽

10.18778/0138-0680.48.2.02 ◽

2019 ◽

Vol 48 (2) ◽

pp. 99-116

Author(s):

Dorota Leszczyńska-Jasion ◽

Yaroslav Petrukhin ◽

Vasilyi Shangin

Keyword(s):

Correspondence Analysis ◽

Boolean Functions ◽

Propositional Logic ◽

Sequent Calculus ◽

Sequent Calculi ◽

Classical Propositional Logic ◽

Logic Of Questions ◽

Proof Systems

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic (i.e. pertaining to the logic of questions) calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for the method of Socratic proofs. Correspondence analysis is Kooi and Tamminga's technique for designing proof systems. In this paper it is used to consider sequent calculi with non-branching (the only exception being the rule of cut), invertible rules for the negation fragment of classical propositional logic and its extensions by binary Boolean functions.

Download Full-text

PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS

The Review of Symbolic Logic ◽

10.1017/s1755020319000261 ◽

2019 ◽

Vol 13 (4) ◽

pp. 720-747

Author(s):

SERGEY DROBYSHEVICH ◽

HEINRICH WANSING

Keyword(s):

Modal Logic ◽

Sequent Calculus ◽

Axiom System ◽

Modal Logics ◽

Cut Elimination ◽

Proof Systems ◽

Image Position ◽

Axiomatic Extension

AbstractWe present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing (2010) and Odintsov & Wansing (2017), as well as the modal logic KN4 with strong implication introduced in Goble (2006). In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown.

Download Full-text