Student research opportunities
Combining Theorem Proving and Constraint Satisfaction
Project Code: CECS_1157
This project is available at the following levels:
Summer Scholar, Masters, PhD
Keywords:
Automated Reasoning, Constraint Satisfaction
Supervisor:
Dr Peter BaumgartnerOutline:
Beagle is an automated theorem prover for first-order logic with equality. Unlike most other theorem provers for first-order logic, it includes specialized reasoning modules for linear arithmetic, so that it can deal with proof problems that involve, e.g., lists or arrays over integers. Beagle is implemented in Scala.
Goals of this project
Beagle's modular theory reasoning interface makes it easy to couple external solvers. Constraint solvers provide efficient algorithms for combinatorial search problems on finite domains. The project asks to couple a constraint solver with Beagle and carry out experiments. A substantial part of the project is also conceptual work on investigating the benefits of the added expressivity of theorem proving and constraint solving.
Requirements/Prerequisites
Working knowledge of Scala (or Java)
Student Gain
Becoming aquainted with and contributing to the state of the art in automated theorem proving techniques
Background Literature
See web links below
Links
Constraint ProgrammingAutomated Theorem Proving
Beagle Theorem Prover
