Eliminating Models During Model Elimination

We investigate the integration of SAT technology into clausal connection-tableau systems for classical first-order logic. Clauses present in tableaux during backtracking search are heuristically grounded and added to an incremental SAT solver. If the solver reports an unsatisfiable set of ground clauses at any point, search may be halted and a proof reported. This technique alone is surprisingly effective, but also supports further refinements “for free”. In particular we further investigate depth control of randomised search based on grounded clauses, and a kind of ground lemmata rule derived from the partial SAT model.