Simplification of Horn Clauses That Are Clausal Forms of Guarded Formulas

Abstract

The guarded fragment of first order logic, defined in [1], has attracted much attention recently due to the fact that it is decidable and several interesting modal logics can be translated into it. Guarded clauses, defined by de Nivelle in [7], are a generalization of guarded formulas in clausal form. In [7], it is shown that the class of guarded clause sets is decidable by saturation under ordered resolution.

In this work, we deal with guarded clauses that are Horn clauses. We introduce the notion of primitive guarded Horn clause: A guarded Horn clause is primitive iff it is either ground and its body is empty, or it contains exactly one body literal which is flat and linear, and its head literal contains a non-ground functional term. Then, we show that every satisfiable and finite set of guarded Horn clauses S can be transformed into a finite set of primitive guarded Horn clauses S′ such that the least Herbrand models of S and S′ coincide on predicate symbols that occur in S.

This transformation is done in the following way: first, de Nivelle’s saturation procedure is applied on the given set S, and certain clauses are extracted form the resulting set. Then, a resolution based technique that introduces new predicate symbols is used in order to obtain the set S′. Our motivation for the presented method is automated model building.