Linear and unit-resulting refutations for Horn theories (Q1923821)

The paper presents an approach to combine two effective resolution strategies for a Horn clause set. The proposed method consists of saturating a Horn clause set under several deduction operations by adding new inference rules until only redundant consequences can be added. This technique -- called linearizing completion -- allows to combine the unit-resulting resolution strategy with a linear strategy à la Prolog in a refutationally complete way. This is not trivial, since although each strategy alone is complete for Horn theories, their naive combination is not. A redundancy criterion allows deletion of many of added inference rules, which makes the resulting inference systems quite compact. The transformed theory can be used in combination with linear calculi, such as, e.g., model elimination, to yield sound, complete and efficient calculi for full first-order clause logic over the given Horn theory. The method has been implemented and has been tested in conjunction with a model-elimination theorem prover.