The relative efficiency of propositional proof systems

1979 ◽  
Vol 44 (1) ◽  
pp. 36-50 ◽  
Author(s):  
Stephen A. Cook ◽  
Robert A. Reckhow
Keyword(s):  
Relative Efficiency ◽  
Natural Deduction ◽  
Type Systems ◽  
Linear Increase ◽  
Proof System ◽  
Proof Systems ◽  
System A ◽  
Frege Systems ◽  
Propositional Proof Systems ◽  
Hilbert Type

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results.In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.

The deduction rule and linear and near-linear proof simulations

1993 ◽  
Vol 58 (2) ◽  
pp. 688-709 ◽  
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).

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

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.

Relational proof system for relevant logics

1992 ◽  
Vol 57 (4) ◽  
pp. 1425-1440 ◽  
Author(s):  
Ewa Orlowska
Keyword(s):  
Natural Deduction ◽  
Proof System ◽  
Algebraic Semantics ◽  
Proof Systems ◽  
Relevant Logics ◽  
Deduction Rules

AbstractA method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.

Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds

2004 ◽  
Vol 69 (1) ◽  
pp. 265-286 ◽  
Author(s):  
Jan Krajíček
Keyword(s):  
Lower Bounds ◽  
Sparse Matrix ◽  
Proof System ◽  
Direct Construction ◽  
Proof Systems ◽  
Circuit Lower Bounds ◽  
Iterable Functions ◽  
Propositional Proof Systems ◽  
Propositional Proof ◽  
Surjective Function

AbstractThis article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like EF. cf. [14, 15]. The particular tautologies we study, the τ-formulas. are obtained from any /poly map g; they express that a string is outside of the range of g, Maps g considered here are particular pseudorandom generators. The ultimate goal is to deduce the hardness of the τ-formulas for at least EF from some general, plausible computational hardness hypothesis.In this paper we introduce the notions of pseudo-surjective and iterable functions (related to free functions of [15]). These two properties imply the hardness of the τ-formulas from the function but unlike the hardness they are preserved under composition and iteration. We link the existence of maps with these two properties to the provability of circuit lower bounds, and we characterize maps g yielding hard τ-formulas in terms of a hitting set type property (all relative to a propositional proof system). We show that a proof system containing EF admits a pseudo-surjective function unless it simulates a proof system WF introduced by Jeřábek [11]. an extension of EF.We propose a concrete map g as a candidate function possibly pseudo-surjective or free for strong proof systems. The map is defined as a Nisan-Wigderson generator based on a random function and on a random sparse matrix. We prove that it is iterable in a particular way in resolution, yielding the output/input ratio n3 −ε (that improves upon a direct construction of Alekhnovich et al. [2]).

scholarly journals On Some Universal Propositional Proof Systems for Many-Valued Logic

2020 ◽  
pp. 21-28
Author(s):  
Artur Khamisyan
Keyword(s):  
Proof System ◽  
Proof Systems ◽  
Propositional Proof Systems ◽  
Propositional Proof

Some uniform Hilbert-like propositional proof system is suggested for all versions of many-valued logic to apply them to 3 versions of 3-valued logic, two of which have only one designated value, and the last one has two designated values

Proof Systems for 3-valued Logics Based on Gödel’s Implication

2021 ◽  
Author(s):  
Arnon Avron
Keyword(s):  
Paraconsistent Logic ◽  
Type System ◽  
Type Systems ◽  
Cut Elimination ◽  
Proof Systems ◽  
Hilbert Type ◽  
Truth Tables

Abstract The logic $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ was introduced in Robles and Mendéz (2014, Logic Journal of the IGPL, 22, 515–538) as a paraconsistent logic which is based on Gödel’s 3-valued matrix, except that Kleene–Łukasiewicz’s negation is added to the language and is used as the main negation connective. We show that $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ is exactly the intersection of $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$, the two truth-preserving 3-valued logics which are based on the same truth tables. (In $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ the set ${\cal D}$ of designated elements is $\{1\}$, while in $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$  ${\cal D}=\{1,0.5\}$.) We then construct a Hilbert-type system which has (MP) for $\to $ as its sole rule of inference, and is strongly sound and complete for $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Then we show how, by adding one axiom (in the case of $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$) or one new rule of inference (in the case of $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$), we get strongly sound and complete systems for $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Finally, we provide quasi-canonical Gentzen-type systems which are sound and complete for those logics and show that they are all analytic, by proving the cut-elimination theorem for them.

scholarly journals A Compositional Proof System on a Category of Labelled Transition Systems

1989 ◽  
Vol 18 (294) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Category Theory ◽  
Proof System ◽  
Parallel Composition ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Proof Systems ◽  
Categorical Logic ◽  
Parallel Processes ◽  
System A ◽  
Categorical Constructions

This paper presents an attempt to cast labelled transition systems, and other models of parallel computation, in a category-theoretic framework. One aim is to use category theory to provide abstract characterisations of constructions like parallel composition valid throughout a range of different models and to provide formal means for translating between different models. Another aim is to exploit the framework of categorical logic to systematise specification languages and the derivation of proof systems for parallel processes. After presenting a category of labelled transition systems, its categorical constructions are used to establish a compositional proof system. A category of properties of transition systems indexed by the category of labelled transition systems is used in forrning the proof system.

scholarly journals What is the Meaning of Proofs?

2020 ◽  
Author(s):  
Sara Ayhan
Keyword(s):  
Natural Deduction ◽  
The Other ◽  
Proof System ◽  
Sequent Calculi ◽  
Singular Terms ◽  
Proof Systems ◽  
Logical Connectives

Abstract The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective. However, what if we go a step further and ask about the meaning of a proof as a whole? In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs. Two questions are central here. First of all, if we have two (syntactically) different derivations, does this always lead to a difference, firstly, in sense, and secondly, in denotation? The other question is about the relation between different kinds of proof systems (here: natural deduction vs. sequent calculi) with respect to this distinction. Do the different forms of representing a proof necessarily correspond to a difference in how the inferential steps are given? In our framework it will be possible to identify denotation as well as sense of proofs not only within one proof system but also between different kinds of proof systems. Thus, we give an account to distinguish a mere syntactic divergence from a divergence in meaning and a divergence in meaning from a divergence of proof objects analogous to Frege’s distinction for singular terms and sentences.

Disjoint NP-Pairs and Propositional Proof Systems

2014 ◽  
Vol 45 (4) ◽  
pp. 59-75 ◽  
Author(s):  
C. Glaßer ◽  
A. Hughes ◽  
A. L. Selman ◽  
N. Wisiol
Keyword(s):  
Proof Systems ◽  
Propositional Proof Systems ◽  
Propositional Proof
Sign in / Sign up

Export Citation Format

Share Document