Student research opportunities
Making Beagle faster
Project Code: CECS_1156
This project is available at the following levels:
Honours, Summer Scholar
Please note that this project is only for undergraduate students.
Keywords:
Automated Reasoning, Subsumption
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 spends much of its time in trying to prove that derived formulas are subsumed by other formulas and hence can be deleted. Beagle would benefit a lot from speeding up this subsumption test. The paper Simple and Efficient Clause Subsumption with Feature Vector Indexing (available at Stephan Schulz' publications page) explains how to do the subsumption test properly. The project asks to implement the ideas in this paper as part of Beagle.
Requirements/Prerequisites
Working knowledge of Scala (or Java) would be useful.
Student Gain
Becoming aquainted with and contributing to the state of the art in automated theorem proving techniques
Background Literature
See links above
