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 条
  • [21] A Sound and Complete Tableaux Calculus for Reichenbach’s Quantum Mechanics Logic
    Pablo Caballero
    Pablo Valencia
    Journal of Philosophical Logic, 2024, 53 : 223 - 245
  • [22] A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
    Hou, Zhe
    Tiu, Alwen
    Gore, Rajeev
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2013), 2013, 8123 : 172 - 187
  • [23] A labelled sequent calculus for BBI: proof theory and proof search
    Hou, Zhe
    Gore, Rajeev
    Tiu, Alwen
    JOURNAL OF LOGIC AND COMPUTATION, 2018, 28 (04) : 809 - 872
  • [24] The λ-Calculus and the Unity of Structural Proof Theory
    Santo, Jose Espirito
    THEORY OF COMPUTING SYSTEMS, 2009, 45 (04) : 963 - 994
  • [25] A proof system for the linear time μ-calculus
    Dax, Christian
    Hofmann, Martin
    Lange, Martin
    FSTTCS 2006: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2006, 4337 : 273 - +
  • [26] Proof nets for the multimodal Lambek calculus
    Moot R.
    Puite Q.
    Studia Logica, 2002, 71 (3) : 415 - 442
  • [27] MECHANICAL PROOF PROCEDURE FOR PROPOSITIONAL CALCULUS
    EHRENFEUCHT, A
    ORLOWSKA, E
    BULLETIN DE L ACADEMIE POLONAISE DES SCIENCES-SERIE DES SCIENCES MATHEMATIQUES ASTRONOMIQUES ET PHYSIQUES, 1967, 15 (01): : 25 - +
  • [28] A GEOMETRIC PROOF OF THE COMPLETENESS OF THE LUKASIEWICZ CALCULUS
    PANTI, G
    JOURNAL OF SYMBOLIC LOGIC, 1995, 60 (02) : 563 - 578
  • [29] Polarized proof-nets and λμ-calculus
    Laurent, O
    THEORETICAL COMPUTER SCIENCE, 2003, 290 (01) : 161 - 188
  • [30] A simple proof of a theorem in the calculus of variations
    Goursat, E.
    TRANSACTIONS OF THE AMERICAN MATHEMATICAL SOCIETY, 1904, 5 (1-4) : 110 - 112
12345