Student research opportunities

Beagle: Constraint Handling Rules

Project Code: CECS_1158

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

Keywords:

Automated Theorem Proving, Constraint Programming

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 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 includes simplification rules for arithmetic terms, e.g.,the term 1+1 is replaced by the term 2. The simplification rules are currently built-in in a hard-coded way. It would be much better to provide the user with a general language for expressing simplification rules as they see fit for their problem. The project goes even further and implement Constraint Handling Rules as a front-end language for specifying constraint solvers.

Requirements/Prerequisites

Working knowledge of Scala (or Java)

Student Gain

Becoming aquainted with and contributing to the state of the art in automated theorem proving techniques

Background Literature

See links above

Links

Constraint Handling Rules
Automated Theorem Proving
Beagle Theorem Prover

Contact: