An Instantiation-Based Theorem Prover for First-Order Programming
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.
Cite
Text
Zawadzki et al. "An Instantiation-Based Theorem Prover for First-Order Programming." Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, 2011.Markdown
[Zawadzki et al. "An Instantiation-Based Theorem Prover for First-Order Programming." Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, 2011.](https://mlanthology.org/aistats/2011/zawadzki2011aistats-instantiationbased/)BibTeX
@inproceedings{zawadzki2011aistats-instantiationbased,
title = {{An Instantiation-Based Theorem Prover for First-Order Programming}},
author = {Zawadzki, Erik and Gordon, Geoffrey and Platzer, Andre},
booktitle = {Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics},
year = {2011},
pages = {855-863},
volume = {15},
url = {https://mlanthology.org/aistats/2011/zawadzki2011aistats-instantiationbased/}
}