Student research opportunities

Improved quantifier elimination for the Beagle theorem prover

Project Code: CECS_918

This project is available at the following levels:
Honours, Summer Scholar, Masters

Keywords:

First-Order Logic, Automated Reasoning

Supervisor:

Dr Peter Baumgartner

Outline:

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, say, lists or arrays over integers.

Beagle uses something called quantifier elimination to deal for arithmetic formulas over the integers. The current implementation of that follows the so-called Cooper's algorithm and is a bit crude. The project asks for a better implementation of an improved algorithm.

Goals of this project

See Description above.

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.
Learning about quantifier elimination.