Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance - Archive ouverte HAL Access content directly
Conference Papers Year : 2021

Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance

(1) , (1, 2, 3) , (4)
1
2
3
4

Abstract

We prove the SOS strategy for first-order resolution to be refutationally complete on a clause set $N$ and set-of-support $S$ if and only if there exists a clause in $S$ that occurs in a resolution refutation from $N\cup S$. This strictly generalizes and sharpens the original completeness result requiring $N$ to be satisfiable. The generalized SOS completeness result supports automated reasoning on a new notion of relevance aiming at capturing the support of a clause in the refutation of a clause set. A clause $C$ is relevant for refuting a clause set $N$ if $C$ occurs in every refutation of $N$. The clause $C$ is semi-relevant if it occurs in some refutation, i.e., if there exists an SOS refutation with set-of-support $S = \{C\}$ from $N\setminus \{C\}$. A clause that does not occur in any refutation from $N$ is irrelevant, i.e., it is not semi-relevant. Our new notion of relevance separates clauses in a proof that are ultimately needed from clauses that may be replaced by different clauses. In this way it provides insights towards proof explanation in refutations beyond existing notions such as that of an unsatisfiable core.

Dates and versions

hal-03516684 , version 1 (07-01-2022)

Identifiers

Cite

Fajar Haifani, Sophie Tourret, Christoph Weidenbach. Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.327-343, ⟨10.1007/978-3-030-79876-5_19⟩. ⟨hal-03516684⟩
25 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More