# An Instantiation-Based Theorem Prover for First-Order Programming

[edit]

Erik Zawadzki,
Geoffrey Gordon,
Andre Platzer
;

Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, PMLR 15:855-863, 2011.

#### Abstract

First-order programming (FOP) is a new representation language that combines the strengths of mixed-integer linear programming (MILP) and first-order logic (FOL). In this paper we describe a novel feasibility proving system for FOP formulas that combines MILP solving with instance-based methods from theorem proving. This prover allows us to perform lifted inference by repeatedly refining a propositional MILP. We prove that this procedure is sound and refutationally complete: if a formula is infeasible our solver will demonstrate this fact in finite time. We conclude by demonstrating an implementation of our decision procedure on a simple first-order planning problem. [pdf][supplementary]

#### Related Material