Comparison of Theorem Provers for Modal Logics — Introduction and Summary

1998 ◽  
pp. 25-26 ◽  
Author(s):  
Peter Balsiger ◽  
Alain Heuerding
Keyword(s):  
Modal Logics ◽  
Theorem Provers

scholarly journals Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

10.29007/cpbz ◽  
2018 ◽  
Author(s):  
Damien Doligez ◽  
Jael Kriener ◽  
Leslie Lamport ◽  
Tomer Libal ◽  
Stephan Merz
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Propositional Modal Logic ◽  
Theorem Provers ◽  
Syntactic Abstraction

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.

scholarly journals Theorem Provers For Every Normal Modal Logic

10.29007/jsb9 ◽  
2018 ◽  
Author(s):  
Tobias Gleißner ◽  
Alexander Steen ◽  
Christoph Benzmüller
Keyword(s):  
Modal Logic ◽  
Higher Order ◽  
Modal Logics ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
Normal Modal Logic ◽  
Theorem Provers

We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used as a preprocessor for turning TPTP THF-compliant the- orem provers into provers for various modal logics. The choice of the concrete modal logic is thereby specified within the problem as a meta-logical statement. This specification for- mat as well as the underlying semantics parameters are discussed, and the implementation and the operation of the tool are outlined.By combining our tool with one or more THF-compliant theorem provers we accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other available prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive, at least for quantified modal logics, as our experiments demonstrate.

scholarly journals HOL Provers for First-order Modal Logics --- Experiments

10.29007/przw ◽  
2018 ◽  
Author(s):  
Christoph Benzmüller
Keyword(s):  
Higher Order ◽  
Modal Logics ◽  
First Order ◽  
Theorem Provers

Higher-order automated theorem provers have been employed to automate first-order modal logics. Extending previous work, an experiment has been carried out to evaluate their collaborative and individual performances.

Modal logics with Belnapian truth values

2010 ◽  
Vol 20 (3) ◽  
pp. 279-304 ◽  
Author(s):  
Serge P Odintsov ◽  
Heinrich Wansing
Keyword(s):  
Modal Logics ◽  
Truth Values

scholarly journals On modal logics arising from scattered locally compact Hausdorff spaces

2019 ◽  
Vol 170 (5) ◽  
pp. 558-577
Author(s):  
Guram Bezhanishvili ◽  
Nick Bezhanishvili ◽  
Joel Lucero-Bryan ◽  
Jan van Mill
Keyword(s):  
Modal Logics ◽  
Hausdorff Spaces ◽  
Locally Compact

Modal logics of domains on the real plane

Studia Logica ◽  
1983 ◽  
Vol 42 (1) ◽  
pp. 63-80 ◽  
Author(s):  
V. B. Shehtman
Keyword(s):  
Modal Logics ◽  
Real Plane ◽  
The Real

Analyzing completeness of axiomatic functional systems for temporal × modal logics

2010 ◽  
Vol 56 (1) ◽  
pp. 89-102 ◽  
Author(s):  
Alfredo Burrieza ◽  
Inmaculada P. de Guzmán ◽  
Emilio Muñoz-Velasco
Keyword(s):  
Modal Logics ◽  
Functional Systems

A Modal Semantics of Negation in Logic Programming

1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani
Keyword(s):  
Modal Logic ◽  
Logic Programming ◽  
Modal Logics ◽  
Kripke Models ◽  
Logic Programs ◽  
Modal Semantics ◽  
Soundness And Completeness ◽  
Modal Completion ◽  
Well Foundedness

The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.

Sign in / Sign up

Export Citation Format

Share Document