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

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 CONDITIONAL BELIEFS: FROM NEIGHBOURHOOD SEMANTICS TO SEQUENT CALCULUS

2018 ◽  
Vol 11 (4) ◽  
pp. 736-779 ◽  
Author(s):  
MARIANNA GIRLANDO ◽  
SARA NEGRI ◽  
NICOLA OLIVETTI ◽  
VINCENT RISCH
Keyword(s):  
Decision Procedure ◽  
Proof Theory ◽  
Sequent Calculus ◽  
Constructive Proof ◽  
Finite Model ◽  
Finite Model Property ◽  
Semantic Completeness ◽  
Multi Agent ◽  
Labelled Sequent Calculus ◽  
Direct Correspondence

AbstractThe logic of Conditional Beliefs (CDL) has been introduced by Board, Baltag, and Smets to reason about knowledge and revisable beliefs in a multi-agent setting. In this article both the semantics and the proof theory for this logic are studied. First, a natural semantics forCDLis defined in terms of neighbourhood models, a multi-agent generalisation of Lewis’ spheres models, and it is shown that the axiomatization ofCDLis sound and complete with respect to this semantics. Second, it is shown that the neighbourhood semantics is equivalent to the original one defined in terms of plausibility models, by means of a direct correspondence between the two types of models. On the basis of neighbourhood semantics, a labelled sequent calculus forCDLis obtained. The calculus has strong proof-theoretic properties, in particular admissibility of contraction and cut, and it provides a decision procedure for the logic. Furthermore, its semantic completeness is used to obtain a constructive proof of the finite model property of the logic. Finally, it is shown that other doxastic operators can be easily captured within neighbourhood semantics. This fact provides further evidence of the naturalness of neighbourhood semantics for the analysis of epistemic/doxastic notions.

scholarly journals Focused Proof-search in the Logic of Bunched Implications

2021 ◽  
pp. 247-267
Author(s):  
Alexander Gheorghiu ◽  
Sonia Marin
Keyword(s):  
Data Structure ◽  
Proof Theory ◽  
Sequent Calculus ◽  
Operational Semantics ◽  
Search Space ◽  
Difficult Problem ◽  
Cut Elimination ◽  
Proof Search ◽  
Nested Sequents

AbstractThe logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.

PROOF ANALYSIS FOR LEWIS COUNTERFACTUALS

2015 ◽  
Vol 9 (1) ◽  
pp. 44-75 ◽  
Author(s):  
SARA NEGRI ◽  
GIORGIO SBARDOLINI
Keyword(s):  
Possible Worlds ◽  
Sequent Calculus ◽  
Deductive System ◽  
Axiomatic System ◽  
Relational Semantics ◽  
Completeness Proof ◽  
Analytic Proof ◽  
Proof Search ◽  
Similarity Relations ◽  
Labelled Sequent Calculus

AbstractA deductive system for Lewis counterfactuals is presented, based directly on the influential generalisation of relational semantics through ternary similarity relations introduced by Lewis. This deductive system builds on a method of enriching the syntax of sequent calculus by labels for possible worlds. The resulting labelled sequent calculus is shown to be equivalent to the axiomatic system VC of Lewis. It is further shown to have the structural properties that are needed for an analytic proof system that supports root-first proof search. Completeness of the calculus is proved in a direct way, such that for any given sequent either a formal derivation or a countermodel is provided; it is also shown how finite countermodels for unprovable sequents can be extracted from failed proof search, by which the completeness proof turns into a proof of decidability.

Relational semantics and a relational proof system for full Lambek calculus

1998 ◽  
Vol 63 (2) ◽  
pp. 623-637 ◽  
Author(s):  
Wendy MacCaull
Keyword(s):  
Proof Theory ◽  
Kripke Semantics ◽  
Substructural Logic ◽  
Lambek Calculus ◽  
Relational Semantics ◽  
Complete Proof ◽  
Proof Search ◽  
Proof Tree ◽  
Relational Logic ◽  
Completeness Theorems

AbstractIn this paper we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a list of conditions on the relations. It is accompanied by a Kripke-style valuation system analogous to that in [11]. Soundness and completeness theorems with respect to FL hold for RelKripke models. Then, in the spirit of the work of Orlowska [14], [15], and Buszkowski and Orlowska [3], we develop relational logic RFL. The adjective relational is used to emphasize the fact that RFL has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in FL is provable if and only if a translation, t(γ1 ● … ● γn ⊃ α)ευu, has a cut-complete fundamental proof tree. This result is constructive: that is, if a cut-complete proof tree for t(γ1 ● … ● γn ⊃ α)ευu is not fundamental, we can use the failed proof search to build a relational countermodel for t(γ1 ● … ● γn ⊃ α)ευu and from this, build a RelKripke countermodel for γ1 ● … ● γn ⊃ α. These results allow us to add FL, the basic substructural logic, to the list of those logics of importance in computer science with a relational proof theory.

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.

Sign in / Sign up

Export Citation Format

Share Document