A proof-search system for the logic of likelihood

2019 ◽  
Vol 28 (3) ◽  
pp. 261-280 ◽  
Author(s):  
R Alonderis ◽  
H Giedra
Keyword(s):  
Decision Procedure ◽  
Sequent Calculus ◽  
Search System ◽  
Proof Search

Abstract The cut-free Gentzen-type sequent calculus LLK for the logic of likelihood (LL) is introduced in the paper. It is proved that the calculus is sound and complete for LL. Using the introduced calculus LLK, a decision procedure for LL is presented.

scholarly journals Brodsky’s coding method for propositional logic

2017 ◽  
Vol 58 (A) ◽  
pp. 1-6
Author(s):  
Romas Alonderis ◽  
Keyword(s):  
Propositional Logic ◽  
Decision Procedure ◽  
Sequent Calculus ◽  
Search Trees ◽  
Proof Search ◽  
Coding Method

Brodsky’s coding method for propositional logic is considered in the paper. Based on the sequent calculus, the method allows us to determine whether an arbitrary sequent is derivable in the calculus without constructing proof-search trees. The coding method, presented in the paper, can be used as a decision procedure for propositional logic.

Cut elimination and complexity bounds for intuitionistic epistemic logic

2020 ◽  
Vol 30 (1) ◽  
pp. 281-294
Author(s):  
Vladimir N Krupski
Keyword(s):  
Epistemic Logic ◽  
Sequent Calculus ◽  
Formal System ◽  
Point Of View ◽  
Cut Elimination ◽  
Polynomial Space ◽  
Complexity Bounds ◽  
Proof Search

Abstract The formal system of intuitionistic epistemic logic (IEL) was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer–Heyting–Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. We prove that IEL is PSPACE-complete.

scholarly journals Deep Proof Search in MELL

10.29007/p1fd ◽  
2018 ◽  
Author(s):  
Ozan Kahramanogullari
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Proof Search ◽  
Proof Construction ◽  
Deep Inference ◽  
Speed Up

The deep inference presentation of multiplicative exponential linear logic (MELL) benefits from a rich combinatoric analysis with many more proofs in comparison to its sequent calculus presentation. In the deep inference setting, all the sequent calculus proofs are preserved. Moreover, many other proofs become available, and some of these proofs are much shorter. However, proof search in deep inference is subject to a greater nondeterminism, and this nondeterminism constitutes a bottleneck for applications. To this end, we address the problem of reducing nondeterminism in MELL by refining and extending our technique that has been previously applied to multiplicative linear logic and classical logic. We show that, besides the nondeterminism in commutative contexts, the nondeterminism in exponential contexts can be reduced in a proof theoretically clean manner. The method conserves the exponential speed-up in proof construction due to deep inference, exemplified by Statman tautologies. We validate the improvement in accessing the shorter proofs by experiments with our implementations.

Motivating the Rules of Sequent Calculus

2017 ◽  
Author(s):  
Neil Tennant
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Natural Isomorphism ◽  
Inductive Definition ◽  
Proof Search ◽  
Definition Of ◽  
Automated Proof

Parallelized elimination rules in natural deduction correspond to Left rules in the sequent calculus; and introduction rules correspond to Right rules. These rules may be construed as inductive clauses in the inductive definition of the notion of sequent proof. There is a natural isomorphism between natural deductions in Core Logic and the sequent proofs that correspond to them. We examine the relations, between sequents, of concentration and dilution; and describe what it is for one sequent to strengthen another. We examine some possible global restrictions on proof-formation, designed to prevent proofs from proving dilutions of sequents already proved by a subproof. We establish the important result that the sequent rules of Core Logic maintain concentration, and we explain its importance for automated proof-search.

A multi-labelled sequent calculus for Topo-Logic

2020 ◽  
Vol 30 (2) ◽  
pp. 663-696
Author(s):  
Ian Shillito
Keyword(s):  
Structural Properties ◽  
Epistemic Logic ◽  
Search Strategy ◽  
Sequent Calculus ◽  
Search Tree ◽  
Topological Spaces ◽  
Label Technique ◽  
Proof Search ◽  
Labelled Sequent Calculus

Abstract We present a labelled sequent calculus for a trimodal epistemic logic exhibitied in Baltag et al. (2017, Logic, Rationality, and Interaction, pp. 330–346), an extension of the so called ‘Topo-Logic’. To the best of our knowledge, our calculus is the first proof-calculus for this logic. This calculus is obtained via an adaptation of the label technique by internalizing a semantics over topological spaces. This internalization leads to the generation of two kinds of labels in our calculus and the labelling of formulae by pairs of labels. These novelties give tools to provide a simple calculus that is intuitively connected to the semantics. We prove that this calculus enjoys many structural properties such as admissibility of cut, admissibility of contraction and invertibility of its rules. Finally, we exhibit a proof search strategy for our calculus that allows us to prove completeness in a direct way by the extraction of a countermodel from a failure of proof. To define this strategy, we design a tool for controlling the generation of labels in the construction of a search tree, although the termination of this strategy is still open.

scholarly journals A labelled sequent calculus for BBI: proof theory and proof search

2015 ◽  
Vol 28 (4) ◽  
pp. 809-872
Author(s):  
Zhé Hóu ◽  
Rajeev Goré ◽  
Alwen Tiu
Keyword(s):  
Proof Theory ◽  
Sequent Calculus ◽  
Proof Search ◽  
Labelled Sequent Calculus

The cost of a cycle is a square

2002 ◽  
Vol 67 (1) ◽  
pp. 35-60 ◽  
Author(s):  
A. Carbone
Keyword(s):  
Lower Bounds ◽  
Polynomial Time ◽  
Heuristic Algorithms ◽  
Sequent Calculus ◽  
Propositional Calculus ◽  
Polynomial Time Algorithm ◽  
Time Algorithm ◽  
Proof Search ◽  
The Cost ◽  
Flow Graphs

AbstractThe logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with (kn+1) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search.

Sign in / Sign up

Export Citation Format

Share Document