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 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.

The project targets to include so-called instantiation heuristics known from a different branch of automated reasoning in order to make the system more complete (in a theoretical sense) and practically more efficient.

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.