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 条
  • [41] A Proof Calculus for Attack Trees in Isabelle
    Kammueller, Florian
    DATA PRIVACY MANAGEMENT, CRYPTOCURRENCIES AND BLOCKCHAIN TECHNOLOGY, 2017, 10436 : 3 - 18
  • [42] Reducing nondeterminism in the calculus of structures
    Kahramanogullari, Ozan
    Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2006, 4246 : 272 - 286
  • [43] Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
    Mizutani, Shinnosuke
    Nishida, Naoki
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (265): : 35 - 51
  • [44] A sound and complete CG proof procedure combining projections with analytic tableaux
    Kerdiles, G
    Salvat, E
    CONCEPTUAL STRUCTURES: FULFILLING PEIRCE'S DREAM, 1997, 1257 : 371 - 385
  • [45] A BIJECTIVE PROOF OF THE HOOK-LENGTH FORMULA FOR STANDARD IMMACULATE TABLEAUX
    Gao, Alice L. L.
    Yang, Arthur L. B.
    PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 2016, 144 (03) : 989 - 998
  • [46] A PROOF CALCULUS WHICH REDUCES SYNTACTIC BUREAUCRACY
    Guglielmi, Alessio
    Gundersen, Tom
    Parigot, Michel
    PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'10), 2010, 6 : 135 - 150
  • [47] On the asymptotic Nullstellensatz and Polynomial calculus proof complexity
    Riis, Soren
    TWENTY-THIRD ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2008, : 272 - 283
  • [48] Categorical proof theory of classical propositional calculus
    Bellin, Gianluigi
    Hyland, Martin
    Robinson, Edmund
    Urban, Christian
    THEORETICAL COMPUTER SCIENCE, 2006, 364 (02) : 146 - 165
  • [49] On the proof theory of Coquand's calculus of constructions
    Seldin, JP
    ANNALS OF PURE AND APPLIED LOGIC, 1997, 83 (01) : 23 - 101
  • [50] Proof nets for basic discontinuous Lambek calculus
    Morrill, Glyn
    Fadda, Mario
    JOURNAL OF LOGIC AND COMPUTATION, 2008, 18 (02) : 239 - 256
12345