Student research opportunities
Instantiation heuristics for the Beagle theorem prover
Project Code: CECS_917
This project is available at the following levels:
Honours, Summer Scholar, Masters
Keywords:
First-Order Logic, Automated Reasoning
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 specialised reasoning modules for (linear) arithmetic, so that it can deal with proof problems that involve, e.g., lists or arrays over integers.
Goals of this project
The project aims to include so-called instantiation heuristics known from a different branch of automated reasoning, SMT-solving, in order to make Beagle practically more useful.
Requirements/Prerequisites
Some background in logic. Good implementation skills. Experiences with Scala desirable.
Student Gain
Become acquainted with first-order logic theorem proving,
in particular from a practical perspective by extending one such system and experimenting with it.
Background Literature
Introductory material on resolution based theorem proving and SMT solving.
Links
Beagle theorem proverAutomated Theorem Proving
