Symmetric blocking

被引：2

作者：

Areces, Carlos ^{[1
,2
]}

Orbe, Ezequiel ^{[1
,2
]}

机构：

[1] Univ Nacl Cordoba, FaMAF, RA-5000 Cordoba, Argentina

[2] Consejo Nacl Invest Cient & Tecn, RA-1033 Buenos Aires, DF, Argentina

来源：

THEORETICAL COMPUTER SCIENCE | 2015年 / 606卷

关键词：

Modal logics; Symmetry; Blocking; Detection; Evaluation; TABLEAUX;

D O I：

10.1016/j.tcs.2015.06.020

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We present three different techniques that use information about symmetries detected in the input formula to block the expansion of diamonds in a modal tableau. We show how these blocking techniques can be included in a standard tableaux calculus for the basic modal logic, and prove that they preserve soundness and completeness. We empirically evaluate these blocking mechanisms in different modal benchmarks. (C) 2015 Elsevier B.V. All rights reserved.

引用

页码：25 / 41

页数：17

共 33 条

[1] Solving difficult instances of Boolean satisfiability in the presence of symmetry [J].

Aloul, FA ;

Ramani, A ;

Markov, IL ;

Sakallah, KA .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2003, 22 (09) :1117-1137

[2]

Areces C, 2000, FR ART INT, V54, P199

[3]

Areces C., 2003, P M4M 3 NANC FRANC

[4]

Areces C, 2013, LECT NOTES ARTIF INT, V8123, P13, DOI 10.1007/978-3-642-40537-2_4

[5]

Audemard G., 2004, P 7 INT C THEOR APPL, P257

[6] A benchmark method for the propositional modal logics K, KT, S4 [J].

Balsiger, P ;

Heuerding, A ;

Schwendimann, S .

JOURNAL OF AUTOMATED REASONING, 2000, 24 (03) :297-317

[7] TRACTABILITY THROUGH SYMMETRIES IN PROPOSITIONAL CALCULUS [J].

BENHAMOU, B ;

SAIS, L .

JOURNAL OF AUTOMATED REASONING, 1994, 12 (01) :89-102

[8]

Blackburn Patrick, 2006, HDB MODAL LOGIC STUD, V3

[9]

Blackburn Patrick, 2001, Cambridge Tracts in Theoretical Computer Science, V53

[10]

Crawford J, 1996, MOR KAUF R, P148

← 1 2 3 4 →