×

Set-blocked clause and extended set-blocked clause in first-order logic. (English) Zbl 1437.03118

Summary: Due to scale and complexity of first-order formulas, simplifications play a very important role in first-order theorem proving, in which removal of clauses and literals identified as redundant is a significant component. In this paper, four types of clauses with the local redundancy property were proposed, separately called a set-blocked clause (SBC), extended set-blocked clause (E-SBC), equality-set-blocked clause (ESBC) and extended equality-set-blocked clause (E-ESBC). The former two are redundant clauses in first-order formulas without equality while the latter two are redundant clauses in first-order formulas with equality. In addition, to prove the correctness of the four proposals, the redundancy of the four kinds of clauses were proved. It was guaranteed eliminating clauses with the four forms has no effect on the satisfiability or the unsatisfiability of original formulas. In the end, effectiveness and confluence properties of corresponding clause elimination methods were analyzed and compared.

MSC:

03B70 Logic in computer science
68T27 Logic in artificial intelligence
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

VAMPIRE; Lingeling
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Järvisalo, M.; Biere, A.; Heule, M.; Blocked clause elimination; International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010): Berlin/Heidelberg, Germany 2010; ,129-144. · Zbl 1284.03208
[2] Heule, M.J.H.; Järvisalo, M.; Biere, A.; Clause elimination procedures for CNF formulas; Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS: Berlin/Heidelberg, Germany 2010; ,357-371. · Zbl 1306.68144
[3] Järvisalo, M.; Heule, M.J.H.; Biere, A.; Inprocessing rules; International Joint Conference on Automated Reasoning (IJCAR-4): Berlin/Heidelberg, Germany 2012; ,355-370. · Zbl 1358.68256
[4] Chen, J.; Fast Blocked Clause Decomposition with High Quality; arXiv: 2015; .
[5] Heule, M.; Biere, A.; Blocked clause decomposition; International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19): Berlin/Heidelberg, Germany 2013; ,423-438. · Zbl 1407.68451
[6] Kiesl, B.; Seidl, M.; Tompits, H.; Biere, A.; Super-Blocked Clauses; International Joint Conference on Automated Reasoning (IJCAR): Cham, Switzerland 2016; ,45-61. · Zbl 1475.68347
[7] Kiesl, B.; Suda, M.; Seidl, M.; Tompits, H.; Biere, A.; Blocked Clauses in First-Order Logic; arXiv: 2017; . · Zbl 1403.68240
[8] Kovács, L.; Voronkov, A.; First-order theorem proving and Vampire; International Conference on Computer Aided Verification (CAV 2013): Berlin/Heidelberg, Germany 2013; ,1-35.
[9] Kiesl, B.; Suda, M.; A unifying principle for clause elimination in first-order logic; International Conference on Automated Deduction (CADE 2017): Cham, Switzerland 2017; ,274-290. · Zbl 1496.03048
[10] Liu, X.; ; Automated Reasoning based on Resolution: Beijing, China 1994; .
[11] Khasidashvili, Z.; Korovin, K.; Predicate elimination for preprocessing in first-order theorem proving; International Conference on Theory and Applications of Satisfiability Testing: Cham, Switzerland 2016; ,361-372. · Zbl 1475.68441
[12] Baader, F.; Nipkow, T.; ; Term Rewriting and All That: Cambridge, UK 1998; . · Zbl 0948.68098
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.