Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover

The main topic of this article are SGGS decision procedures for fragments of first-order logic without equality. SGGS (Semantically-Guided Goal-Sensitive reasoning) is an attractive basis for decision procedures, because it generalizes to first-order logic the Conflict-Driven Clause Learning (CDCL) procedure for propositional satisfiability. As SGGS is both refutationally complete and model-complete in the limit, SGGS decision procedures are model-constructing. We investigate the termination of SGGS with both positive and negative results: for example, SGGS decides Datalog and the stratified fragment (including Effectively PRopositional logic) that are relevant to many applications. Then we discover several new decidable fragments, by showing that SGGS decides them. These fragments have the small model property, as the cardinality of their SGGS-generated models can be upper bounded, and for most of them termination tools can be applied to test a set of clauses for membership. We also present the first implementation of SGGS - the Koala theorem prover - and we report on experiments with Koala.