Carnegie Mellon University
file.pdf (366.77 kB)

An Instantiation-Based Theorem Prover for First-Order Programming

Download (366.77 kB)
journal contribution
posted on 2011-01-01, 00:00 authored by Erik Zawadski, Geoffrey J. Gordon, Andre Platzer

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.


Publisher Statement

Copyright 2011 by the authors



Usage metrics