In: Proceedings of the 11th International Conference on Application and Theory of Petri Nets, 1990, Paris, France, pages 411-430. 1990.
Abstract: The paper provides a Petri net-based analysis of the satisfiability problem in the Horn clause propositional logic: Given a set H of Horn clauses and a query Q, determine whether or not Q is satifiable over H.
Assuming that Q is not satisfiable over H, the problem of finding a smallest modifiction to obtain a query Q' and a set H' of Horn clauses over which Q' is satisfiable is considered, and the minimum modification by variable deletion, by clause addition or by their combination is shown to be intractable. Approximation algorithms and experimantal results are alo presented.
Keywords: satisfiability problem (in the) Horn clause propositional logic.