Student research opportunities
Coupling Beagle with Darwin
Project Code: CECS_1159
This project is available at the following levels:
Honours, Summer Scholar
Please note that this project is only for undergraduate students.
Keywords:
Automated Theorem Proving, First-Order Logic
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. In particular, the external solver can be a theorem prover itself, and the project asks to couple the E-Darwin prover. This makes sense as it allows one to exploit the rather complementary capabilities of Beagle and E-Darwin.
Requirements/Prerequisites
Working Knowlege of Scala (Java)
Student Gain
Becoming aquainted with and contributing to the state of the art in automated theorem proving techniques
Background Literature
See links above and below
Links
Automated Theorem ProvingBeagle Theorem Prover
