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 条
  • [1] A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules
    Cassano, Valentin
    Lopez Pombo, Carlos Gustavo
    Maibaum, Thomas S. E.
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2015), 2015, 9323 : 6 - 21
  • [2] EXPTIME TABLEAUX FOR THE COALGEBRAIC μ-CALCULUS
    Cirstea, Corina
    Kupke, Clemens
    Pattinson, Dirk
    LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (03)
  • [3] EXPTIME Tableaux for the Coalgebraic μ-Calculus
    Cirstea, Corina
    Kupke, Clemens
    Pattinson, Dirk
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2009, 5771 : 179 - +
  • [4] A tableaux calculus for ambiguous quantification
    Monz, C
    de Rijke, M
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1998, 1397 : 232 - 246
  • [5] A Preferential Tableaux Calculus for Circumscriptive ALCO
    Grimm, Stephan
    Hitzler, Pascal
    WEB REASONING AND RULE SYSTEMS, PROCEEDINGS, 2009, 5837 : 40 - +
  • [6] A Tableaux Calculus for Default Intuitionistic Logic
    Cassano, Valentin
    Fervari, Raul
    Hoffmann, Guillaume
    Areces, Carlos
    Castro, Pablo F.
    AUTOMATED DEDUCTION, CADE 27, 2019, 11716 : 161 - 177
  • [7] Tableaux and sequent calculus for minimal entailment
    Olivetti, Nicola
    Journal of Automated Reasoning, 1992, 9 (01)
  • [8] Proof output and transformation for disconnection tableaux
    Correll, P
    Stenz, G
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2005, 3702 : 312 - 317
  • [9] Unranked Tableaux Calculus for Web Related Applications
    Dundua, Besik
    Kurtanidze, Lia
    Rukhaia, Mikheil
    2017 IEEE FIRST UKRAINE CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING (UKRCON), 2017, : 1181 - 1184
  • [10] A NEW PROOF OF THE REALISATION OF CUBIC TABLEAUX
    Yang, Fei
    Yin, Yongcheng
    BULLETIN OF THE AUSTRALIAN MATHEMATICAL SOCIETY, 2013, 87 (02) : 207 - 215
12345