In: Proceedings of the IEEE International Symposium on Circuits and Systems, 1990, New Orleans, LA, USA; Part 4, pages 2662-2665. Piscataway, NJ, USA: IEEE Service Center, 1990.
Abstract: A Petri-net-based algorithm for the satisfiability problem in the Horn clause propositional logic is presented. The problem is defined by: given a set H of Horn clauses and a query Q, determine whether or not Q is satisfiable over H. An O(vēc) algorithm for finding a proof procedure of the problem, where v and c are the numbers of variables and clauses, respectively, is proposed. The time complexity of the following problem is analyzed: finding a smallest modification to obtain a query Q' and a set H' of Horn clauses over which Q' is satisfiable if Q is not satisfiable over H. Approximation algorithms are presented.
Keywords: net-based algorithm (for) proofs (in) Horn clause propositional logic; satisfiability problem (in) Horn clause propositional logic; time complexity.