Automating natural deduction proofs

Research areas

Temporary Supervisor

Professor John Slaney

Description

It is proposed to devise, implement and test a set of tools intended to help in undergraduate education in elementary logic. Specifically, there needs to be software which efficiently finds proofs of sequents in first order logic and presents them in a standard natural deduction format. Deep and complicated problems are not the issue: the program needs to solve easy problems fast. Secondly, there needs to be a web-based tool which helps students devise their own proofs by checking what they enter, line by line, and providing helpful error messages when things go wrong. Both tools are intended to be deployed in actual logic teaching at the ANU and online for outside students. These could be two separate projects, or could be combined into one.

Goals

Student-friendly theorem prover and proof assistant for first order natural deduction, intended to help in teaching basic logic at the undergraduate level.

Requirements

Must have passed COMP2620 with at least Distinction. Programming ability is essential. Existing web interface is written in Python. Back-end theorem prover could be in any language, but needs to run fast.

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing