A Petri net-based algorithm for proofs in Horn clause propositional logic

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(ν²c) algorithm for determining whether or not Q is satisfiable over H is proposed. An O (ν2^ν) algorithm for finding a proof procedure of the problem, where ν 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 and experimental results are presented