Semantic Relevance - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Semantic Relevance

Résumé

Abstract A clause C is syntactically relevant in some clause set N , if it occurs in every refutation of N . A clause C is syntactically semi-relevant, if it occurs in some refutation of N . While syntactic relevance coincides with satisfiability (if C is syntactically relevant then $$N\setminus \{C\}$$ N \ { C } is satisfiable), the semantic counterpart for syntactic semi-relevance was not known so far. Using the new notion of a conflict literal we show that for independent clause sets N a clause C is syntactically semi-relevant in the clause set N if and only if it adds to the number of conflict literals in N . A clause set is independent, if no clause out of the clause set is the consequence of different clauses from the clause set. Furthermore, we relate the notion of relevance to that of a minimally unsatisfiable subset (MUS) of some independent clause set N . In propositional logic, a clause C is relevant if it occurs in all MUSes of some clause set N and semi-relevant if it occurs in some MUS. For first-order logic the characterization needs to be refined with respect to ground instances of N and C .
Fichier principal
Vignette du fichier
paper.pdf (328.17 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03881904 , version 1 (02-12-2022)

Identifiants

Citer

Fajar Haifani, Christoph Weidenbach. Semantic Relevance. IJCAR, International Joint Conference in Automated Reasoning, Aug 2022, Haifa, Israel. pp.208-227, ⟨10.1007/978-3-031-10769-6_13⟩. ⟨hal-03881904⟩
12 Consultations
17 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More