Model Checking Algorithm for Repairing Inference between Conjunctive Forms

Abstract

Let K be a propositional formula and let ? be a query, the propositional inference problem K |= ? is a Co-NP-complete problem for propositional formulas without restrictions. We show the existence of polynomial-time cases for some fragments of propositional formulas K and ? that are different from the already known case of Horn formulas. For example, in the case that K is a formula in the fragment Krom or Horn or Monotone, then K |= ? can be decided in polynomial-time for any CNF ?. Given two conjunctive normal forms (CNF’s) K and ?, when K ?|= ?, our proposal builds a minimal set of independent clauses S. The falsifying assignments of S are exactly the subset of models of K, which are not models for ?. In this way, the CNF S could extend the initial formula K in such a way that repair the inference, it is (S ? K) |= ? is held.