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( nu /sup 2/c) algorithm for determining whether or not Q is satisfiable over H is proposed. An O( nu 2/sup nu /) algorithm for finding a proof procedure of the problem, where nu 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.