Subsumption Algorithms for Three-Valued Geometric Resolution

In an implementation of geometric resolution, the most costly operation is subsumption (or matching): One has to decide for a three-valued, geometric formula, whether this formula is false in a given interpretation. The formula contains only atoms with variables, equality, and existential quantifiers. The interpretation contains only atoms with constants. Because the atoms have no term structure, matching for geometric resolution is a hard problem. We translate the matching problem into a generalized constraint satisfaction problem, and give an algorithm that solves it efficiently. The algorithm uses learning techniques, similar to clause learning in propositional logic. Secondly, we adapt the algorithm in such a way that it finds solutions that use a minimal subset of the interpretation. The techniques presented in this paper may have applications in constraint solving.