An Instantiation-Based Theorem Prover for First-Order Programming


Erik Zawadzki, Geoffrey Gordon, Andre Platzer ;
Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, PMLR 15:855-863, 2011.


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