2011
AISTATS
AISTATS 2011
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.
🌉
Interdisciplinary Bridge
— Artificial Intelligence and Mathematics & Optimization
📈
Trend Setter
— Discrete Mathematics
🧭
Keyword Pioneer
— theorem proving
🐝
Cross-Pollinator
— Artificial Intelligence, Deep Learning, Knowledge & Reasoning, Machine Learning, Mathematics & Optimization, Natural Language Processing, Reinforcement Learning
🐣
Hot Topic Early Bird
— first-order logic