Trinity College Dublin

Department of Computer Science > UTP Proof Assistant

	Andrew Butterfield
	FMG Home
	U·(TP)² Sources
	U·(TP)² Binaries

U·(TP)² Home

Introduction

This theorem prover is being deprecated, while a new version is being built from scratch. The new version is being devleloped using stack, on a Mac OS X platform. The most recent and useable version of this is the one used for the 2013-14 CS4003 course in the UTP-2014 Archive

Unifying Theories of Programming Theorem Prover ( U·(TP)², "UTP-squared", or UTP2 if stuck in ASCII-land ) is a theorem proving assistant for 2nd-order predicate calculus, designed to support foundational proof work in the Unifying Theories of Programming framework (UTP).

Formerly known as Saoithín (pronounced "See-heen").

Background

Documentation under preparation (these are very rough, very thin drafts)

Reference Manual (21 Nov 2013, 32 pages, logic mathematical syntax, free-variable sets, substitution, some axioms, inference rules, and derived rules)
User Guide (21 Nov 2013, 11 pages, some math and ASCII syntax information)
Hacker's Guide (21 Nov 2013, 16 pages, shows literate script format, directory structure and the key text files for installation. Also some stuff about the parser grammar.

Papers:

UTP 2010, Shanghai, Nov. 2010

UTP 2012, Paris, Aug. 2012

A Slide Presentation (PDF) gives the motivation behind the decision to develop this tool.

Implementation

U·(TP)² is implemented in Haskell, (GHC 6.10.4) using the wxHaskell package (0.11.1.2) for its GUI interface. We also use the Parsec library to implement the plain-text predicate parsing facilities, and have modified Jaza to handle the LaTeX parser facilities.

It has been successfully developed and tested using GHCi on:

300Mhz Pentium III, Windows 98
2.5Ghz Pentium IV, Windows XP SP2
2.8Ghz Intel Duo, Vista Home Edition
2.6Ghz Intel Duo, Windows XP SP2
2.6Ghz Intel Duo, Windows7
2.93Ghz Intel Core i7 Mac (OS X) , in Windows 7 on both a VMWare Fusion virtual machine and a Dell XT-3 Tablet.

Students at TCD have successfully built it on Linux (Ubuntu). It should run in principle on Max OS X as well, but I have not been able to get this to work (help would be appreciated).

Distributions

Sources

The sources are managed using Mercurial and are available under GPL v2.

TCD Repository, whose "tip" will always be code that compiles and runs (but may not be bug-free!)

Bitbucket repository, which is the active working repo., and may (not often) contain code that is broken.

tagged versions

current TODO file

Binary Bundles and Executables

Windows

The zip files in the table below are complete releases. Executable files on their own can be simply dropped in on top of the most recent full release, replacing the existing executable. So, to install the latest version, download the most recent ZIP, followed by the most recent EXE.

The executable has now been renamed from "Saoithin.exe" to "UTP2.exe".

Date	Version	ZIP	Executable	Comments
04-DEC-2013	0.97α9		EXE	CS4003 2013 Feedback
15-NOV-2013	0.97α8	ZIP		CS4003 2013 Release
12-DEC-2012	0.96α5		EXE	CS4003 Bugfix 2 Release
16-NOV-2012	0.96α4	ZIP		CS4003 2012 Bugfix 1 Release
07-JUN-2012	0.94α5	ZIP	EXE	Long overdue release !
07-APR-2011	0.91α3		EXE	α-equivalence crash fix
14-MAR-2011	0.90α6		EXE	data entry/type checking fix
24-FEB-2011	0.90α5	ZIP		CS3001 2011 Initial Release
15-Nov-2010	0.88α3	ZIP		UTP 2010 initial version
18-Oct-2010	0.88α1	ZIP		minor style file fix
04-Oct-2010	0.88α		EXE	Law provenance added
8-Sep-2010	0.87α	ZIP		Theory create/edit now supported
24-Aug-2010	0.86α10		EXE	version cited in UTP2010 paper
19-Jul-2010	0.86α3	ZIP
9-Jul-2010	0.86α2	ZIP		screenshots in UTP2010 paper

Unix

... if some kind soul can build these for me, I'll host them here..

Mac OS/X