Ground resolution with group computations on semantic symmetries

Abstract

The shift to semantic symmetries is motivated by the fact that, in contrast with syntactic symmetries, these are preserved under standard inference rules such as resolution. It is then possible to attach groups of semantic symmetries to sets of ground clauses. These groups can provide information useful to inference, as illustrated by three “symmetric” rules. These rules are to be applied in well-defined, disjoint cases, they simplify both the set of clauses and the attached group, they use standard and efficient techniques from computational group theory, and therefore they can be easily mechanised. A prototype GAP implementation is described, and an example developed. Finally, some complexity results concerning the computation of semantic symmetries are given.