MleanCoP: A Connection Prover for First-Order Modal Logic

被引：0
|
作者：
Otten, Jens [1 ]
机构：
[1] Univ Potsdam, Inst Informat, D-14482 Potsdam, Germany
来源：
AUTOMATED REASONING, IJCAR 2014 | 2014年 / 8562卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
MleanCoP is a fully automated theorem prover for first-order modal logic. The proof search is based on a prefixed connection calculus and an additional prefix unification, which captures the Kripke semantics of different modal logics. MleanCoP is implemented in Prolog and the source code of the core proof search procedure consists only of a few lines. It supports the standard modal logics D, T, S4, and S5 with constant, cumulative, and varying domain conditions. The most recent version also supports heterogeneous multimodal logics and outputs a compact prefixed connection proof. An experimental evaluation shows the strong performance of MleanCoP.
引用
收藏
页码：269 / 276
页数：8
相关论文
共 50 条
  • [1] Connecting a logical framework to a first-order logic prover
    Abel, A
    Coquand, T
    Norell, U
    [J]. FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2005, 3717 : 285 - 301
  • [2] First-order classical modal logic
    Arló-Costa H.
    Pacuit E.
    [J]. Studia Logica, 2006, 84 (2) : 171 - 210
  • [3] FIRST-ORDER DEFINABILITY IN MODAL LOGIC
    GOLDBLATT, RI
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1975, 40 (01) : 35 - 40
  • [4] αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic
    Near, Joseph P.
    Byrd, William E.
    Friedman, Daniel P.
    [J]. LOGIC PROGRAMMING, PROCEEDINGS, 2008, 5366 : 238 - 252
  • [5] Unification in first-order transitive modal logic
    Dzik, Wojciech
    Wojtylak, Piotr
    [J]. LOGIC JOURNAL OF THE IGPL, 2019, 27 (05) : 693 - 717
  • [6] A FIRST-ORDER FRAMEWORK FOR INQUISITIVE MODAL LOGIC
    Meissner, Silke
    Otto, Martin
    [J]. REVIEW OF SYMBOLIC LOGIC, 2022, 15 (02): : 311 - 333
  • [7] On the Expressivity of First-Order Modal Logic with "Actually"
    Kocurek, Alexander W.
    [J]. LOGIC, RATIONALITY, AND INTERACTION (LORI 2015), 2015, 9394 : 207 - 219
  • [8] iProver - An instantiation-based theorem prover for first-order logic
    Korovin, Konstantin
    [J]. AUTOMATED REASONING, PROCEEDINGS, 2008, 5195 : 292 - 298
  • [9] A model generation based theorem prover MGTP for first-order logic
    Hasegawa, Ryuzo
    Fujita, Hiroshi
    Koshimura, Miyuki
    Shirai, Yasuyuki
    [J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2002, 2408 (PART2): : 178 - 213
  • [10] A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness
    From, Asta Halkjaer
    Villadsen, Jorgen
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023, 2023, 14278 : 468 - 480
12345