Personal tools
You are here: Home News LFCS Lab Lunch by John Longley

LFCS Lab Lunch by John Longley

Theorem proving as a computer game

What
When May 28, 2013
from 01:00 PM to 02:00 PM
Where MF2
Add event to calendar vCal
iCal

I will describe and demonstrate a simple interactive theorem prover that has resulted from a succession of student projects I have recently supervised.

The tool uses a graphical presentation of proof states based loosely on a football metaphor, and allows entirely mouse-driven proofs of simple theorems in Hilbert's Primitive Recursive Arithmetic.

Document Actions