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.

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 this Paper

BibTeX
@InProceedings{pmlr-v15-zawadzki11a, 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}, pages = {855--863}, year = {2011}, editor = {Gordon, Geoffrey and Dunson, David and Dudík, Miroslav}, volume = {15}, series = {Proceedings of Machine Learning Research}, address = {Fort Lauderdale, FL, USA}, month = {11--13 Apr}, publisher = {PMLR}, pdf = {http://proceedings.mlr.press/v15/zawadzki11a/zawadzki11a.pdf}, url = {https://proceedings.mlr.press/v15/zawadzki11a.html}, 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.} }
Endnote
%0 Conference Paper %T An Instantiation-Based Theorem Prover for First-Order Programming %A Erik Zawadzki %A Geoffrey Gordon %A Andre Platzer %B Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics %C Proceedings of Machine Learning Research %D 2011 %E Geoffrey Gordon %E David Dunson %E Miroslav Dudík %F pmlr-v15-zawadzki11a %I PMLR %P 855--863 %U https://proceedings.mlr.press/v15/zawadzki11a.html %V 15 %X 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.
RIS
TY - CPAPER TI - An Instantiation-Based Theorem Prover for First-Order Programming AU - Erik Zawadzki AU - Geoffrey Gordon AU - Andre Platzer BT - Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics DA - 2011/06/14 ED - Geoffrey Gordon ED - David Dunson ED - Miroslav Dudík ID - pmlr-v15-zawadzki11a PB - PMLR DP - Proceedings of Machine Learning Research VL - 15 SP - 855 EP - 863 L1 - http://proceedings.mlr.press/v15/zawadzki11a/zawadzki11a.pdf UR - https://proceedings.mlr.press/v15/zawadzki11a.html AB - 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. ER -
APA
Zawadzki, E., Gordon, G. & Platzer, A.. (2011). An Instantiation-Based Theorem Prover for First-Order Programming. Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, in Proceedings of Machine Learning Research 15:855-863 Available from https://proceedings.mlr.press/v15/zawadzki11a.html.

Related Material