An algorithm to compute maximal contractions for Horn clauses (Q543196)

In this paper the authors address the problem of computing maximal subsets of a set \(\Gamma\) of formulae which are consistent with a set \(\Delta\) of facts (i.e. maximal contractions). For this, the authors proceed as follows: {\parindent=6,5mm \begin{itemize}\item[(1)] They prove a conversion relationship between minimal inconsistent sets of the union of \(\Gamma\) and \(\Delta\) and maximal contractions. \item[(2)] They give a necessary condition of a set of Horn clauses to be minimal inconsistent. \item[(3)] Based on these two results, they give an algorithm for enumerating all minimal inconsistent subsets of a given set of Horn clauses, and an algorithm for computing the maximal contractions from these minimal inconsistent subsets. \item[(4)] They propose an (interactive) algorithm for computing maximal contractions for Horn clauses by composing the above algorithms. \end{itemize}}