Skip to main content »

Trinity College Dublin

Dublin University Crest Department of Computer Science > UTP Proof Assistant Trinity College Crest
 Andrew Butterfield
 FMG Home
 U·(TP)2 Sources
 U·(TP)2 Binaries
 

U·(TP)2 Home

Introduction

Unifying Theories of Programming Theorem Prover ( U·(TP)2, "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:

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

Implementation

U·(TP)2 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:

  1. 300Mhz Pentium III, Windows 98
  2. 2.5Ghz Pentium IV, Windows XP SP2
  3. 2.8Ghz Intel Duo, Vista Home Edition
  4. 2.6Ghz Intel Duo, Windows XP SP2
  5. 2.6Ghz Intel Duo, Windows7
  6. 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

... if some kind soul can build these for me, I'll host them here..
Email  WebAdmin @ cs.tcd.ie