How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi

2002 ◽  
Author(s):  
A. Voronkov
Keyword(s):  
Modal Logics ◽  
Sequent Calculi ◽  
Proof Search

Proof-search and countermodel generation for non-normal modal logics: The theorem prover PRONOM

2021 ◽  
Vol 14 (2) ◽  
pp. 215-229
Author(s):  
Tiziano Dalmonte ◽  
Sara Negri ◽  
Nicola Olivetti ◽  
Gian Luca Pozzato
Keyword(s):  
Modal Logics ◽  
Experimental Results ◽  
Theorem Prover ◽  
Basic System ◽  
Sequent Calculi ◽  
Modal Formula ◽  
Left Hand ◽  
Proof Search ◽  
The Right ◽  
Normal Modal Logics

In this work we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics. PRONOM implements some labelled sequent calculi recently introduced for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of leanTAP and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having a sequent with an empty left-hand side and containing only that formula on the right-hand side as a root, otherwise PRONOM is able to extract a model falsifying it from an open, saturated branch. The paper shows some experimental results, witnessing that the performances of PRONOM are promising.

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.

Modular Sequent Calculi for Classical Modal Logics

Studia Logica ◽  
2014 ◽  
Vol 103 (1) ◽  
pp. 175-217 ◽  
Author(s):  
David R. Gilbert ◽  
Paolo Maffezioli
Keyword(s):  
Modal Logics ◽  
Sequent Calculi

How to optimize proof-search in modal logics

2001 ◽  
Vol 2 (2) ◽  
pp. 182-215 ◽  
Author(s):  
Andrei Voronkov
Keyword(s):  
Modal Logics ◽  
Proof Search

scholarly journals Proof theory for quantified monotone modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 478-506
Author(s):  
Sara Negri ◽  
Eugenio Orlandelli
Keyword(s):  
Proof Theory ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Completeness Proof ◽  
First Order ◽  
Constant Domains ◽  
Normal Modal Logics ◽  
Order Extension

Abstract This paper provides a proof-theoretic study of quantified non-normal modal logics (NNML). It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut.

Sign in / Sign up

Export Citation Format

Share Document