Lower bounds to the size of constant-depth propositional proofs

1994 ◽  
Vol 59 (1) ◽  
pp. 73-86 ◽  
Author(s):  
Jan Krajíček
Keyword(s):  
Lower Bounds ◽  
Propositional Logic ◽  
Sequent Calculus ◽  
Pigeonhole Principle ◽  
Constant Depth ◽  
Total Size ◽  
Natural Modification ◽  
Gentzen Sequent Calculus

AbstractLK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and ∧,∨ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set of depth d sequents of total size O(n3+d) which are refutable in LK by depth d + 1 proof of size exp(O(log2n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets express a weaker form of the pigeonhole principle.

Gentzen sequent calculi for some intuitionistic modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 596-623
Author(s):  
Zhe Lin ◽  
Minghui Ma
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Intuitionistic Propositional Logic ◽  
Propositional Language ◽  
Intuitionistic Modal Logics ◽  
Subformula Property ◽  
Gentzen Sequent Calculus

Abstract Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond ,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond ,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

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).

scholarly journals Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽  
2019 ◽  
Vol 8 (4) ◽  
pp. 115 ◽  
Author(s):  
Joanna Golińska-Pilarek ◽  
Magdalena Welle
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Classical Propositional Logic ◽  
Tableau System ◽  
Soundness And Completeness

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.

scholarly journals The Method of Socratic Proofs Meets Correspondence Analysis

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.

Lower Bounds for the Weak Pigeonhole Principle Beyond Resolution

2001 ◽  
pp. 1005-1016 ◽  
Author(s):  
Albert Atserias ◽  
Marìa Luisa Bonet ◽  
Juan Luis Esteban
Keyword(s):  
Lower Bounds ◽  
Pigeonhole Principle

scholarly journals Elimination of network intrusions via a resource oriented BDI architecture

2018 ◽  
Vol 8 (1) ◽  
pp. 173-181 ◽  
Author(s):  
Ján Perháč ◽  
Daniel Mihályi ◽  
Lukáš Maťaš
Keyword(s):  
Intrusion Detection System ◽  
Sequent Calculus ◽  
Detection System ◽  
Rational Agent ◽  
Network Intrusion Detection ◽  
Network Intrusion ◽  
Network Intrusions ◽  
Bdi Architecture ◽  
Bdi Logic ◽  
Gentzen Sequent Calculus

Abstract We propose a resource-oriented architecture of a rational agent for a network intrusion detection system. This architecture describes the behavior of a rational agent after detection of unwanted network activities. We describe the creation of countermeasures to ward off detected threats. Examples are created based on the proposed architecture, describing the process during a rational agent detection. We have described these examples by linear BDI logic behavioral formulæ, that have been proven by Gentzen sequent calculus.

scholarly journals Lower Bounds and Separations for Constant Depth Multilinear Circuits

2009 ◽  
Vol 18 (2) ◽  
pp. 171-207 ◽  
Author(s):  
Ran Raz ◽  
Amir Yehudayoff
Keyword(s):  
Lower Bounds ◽  
Constant Depth

scholarly journals Uniform derandomization from pathetic lower bounds

2012 ◽  
Vol 370 (1971) ◽  
pp. 3512-3535 ◽  
Author(s):  
Eric Allender ◽  
V. Arvind ◽  
Rahul Santhanam ◽  
Fengming Wang
Keyword(s):  
Word Problem ◽  
Lower Bounds ◽  
Black Box ◽  
Arithmetic Circuits ◽  
List Type ◽  
Probabilistic Algorithms ◽  
Constant Depth ◽  
Subexponential Time ◽  
Polynomial Size ◽  
Threshold Circuits

The notion of probabilistic computation dates back at least to Turing, who also wrestled with the practical problems of how to implement probabilistic algorithms on machines with, at best, very limited access to randomness. A more recent line of research, known as derandomization, studies the extent to which randomness is superfluous. A recurring theme in the literature on derandomization is that probabilistic algorithms can be simulated quickly by deterministic algorithms, if one can obtain impressive (i.e. superpolynomial, or even nearly exponential) circuit size lower bounds for certain problems. In contrast to what is needed for derandomization, existing lower bounds seem rather pathetic. Here, we present two instances where ‘pathetic’ lower bounds of the form n 1+ ϵ would suffice to derandomize interesting classes of probabilistic algorithms. We show the following: — If the word problem over S 5 requires constant-depth threshold circuits of size n 1+ ϵ for some ϵ >0, then any language accepted by uniform polynomial size probabilistic threshold circuits can be solved in subexponential time (and, more strongly, can be accepted by a uniform family of deterministic constant-depth threshold circuits of subexponential size). — If there are no constant-depth arithmetic circuits of size n 1+ ϵ for the problem of multiplying a sequence of n  3×3 matrices, then, for every constant d , black-box identity testing for depth- d arithmetic circuits with bounded individual degree can be performed in subexponential time (and even by a uniform family of deterministic constant-depth AC 0 circuits of subexponential size).

Sign in / Sign up

Export Citation Format

Share Document