Semantically-guided goal-sensitive theorem proving

We present a new inference system for first-order logic, named SGGS, which stands for semantically-guided goal-sensitive theorem proving. Similar to other instance-based methods, SGGS was inspired by the idea of generalizing the reasoning of the Davis-Putnam-Logemann-Loveland (DPLL) procedure to first-order logic. A double challenge is to achieve this without having to enumerate ground terms, which is inefficient, especially when there are many function and constant symbols, and without adopting depth-first search with backtracking, which works well at the propositional level, but typically causes too much backtracking at the first-order level. SGGS avoids enumeration and is proof confluent, so that it meets both challenges. Furthermore, SGGS is semantically guided, because it is equipped with an initial interpretation. We prove that SGGS is refutationally complete, by showing that it is guaranteed to find a contradiction whenever the input clause set is unsatisfiable, and goal-sensitive, if the initial interpretation is properly chosen.