A Tableaux Calculus for Reducing Proof Size

被引：1
|
作者：
Lettmann, Michael Peter [1 ]
Peltier, Nicolas [2 ]
机构：
[1] Tech Univ Wien, Inst Log & Computat, Vienna, Austria
[2] Univ Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000 Grenoble, France
来源：
AUTOMATED REASONING, IJCAR 2018 | 2018年 / 10900卷
关键词：
D O I：
10.1007/978-3-319-94205-6_5
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
A tableau calculus is proposed, based on a compressed representation of clauses, where literals sharing a similar shape may be merged. The inferences applied on these literals are fused when possible, which can reduce the size of the proof. It is shown that the obtained proof procedure is sound, refutationally complete and can reduce the size of the tableau by an exponential factor. The approach is compatible with all usual refinements of tableaux.
引用
收藏
页码：64 / 80
页数：17
相关论文
共 50 条
  • [31] Semantics and Proof Theory of the Epsilon Calculus
    Zach, Richard
    LOGIC AND ITS APPLICATIONS (ICLA 2017), 2017, 10119 : 27 - 47
  • [32] Proof Nets and the Linear Substitution Calculus
    Accattoli, Beniamino
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2018, 2018, 11187 : 37 - 61
  • [33] The λ-Calculus and the Unity of Structural Proof Theory
    José Espírito Santo
    Theory of Computing Systems, 2009, 45 : 963 - 994
  • [34] A Streamlined Proof of an Essential Calculus Fact
    Walk, Stephen M.
    AMERICAN MATHEMATICAL MONTHLY, 2010, 117 (09): : 832 - 833
  • [35] A proof of the leftmost reduction theorem for λβη-calculus
    Ishii, Katsumasa
    THEORETICAL COMPUTER SCIENCE, 2018, 747 : 26 - 32
  • [36] Proof System for Applied Pi Calculus
    Liu, Jia
    Lin, Huimin
    THEORETICAL COMPUTER SCIENCE, 2010, 323 : 229 - 243
  • [37] A SIMPLE PROOF OF A BASIC THEOREM OF CALCULUS
    POWDERLY, M
    AMERICAN MATHEMATICAL MONTHLY, 1963, 70 (05): : 544 - &
  • [38] THE PROOF-INTUITIONISTIC PROPOSITIONAL CALCULUS
    KUZNETSOV, AV
    DOKLADY AKADEMII NAUK SSSR, 1985, 283 (01): : 27 - 30
  • [39] PROOF SEARCH IN THE INTUITIONISTIC SEQUENT CALCULUS
    SHANKAR, N
    LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 607 : 522 - 536
  • [40] Nested Proof Search as Reduction in the λ-calculus
    Guenot, Nicolas
    PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING, 2011, : 183 - 193
12345