|Department of Computer Science > UTP Proof Assistant|
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)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").
Documentation under preparation (these are very rough, very thin drafts)
A Slide Presentation (PDF) gives the motivation behind the decision to develop this tool.
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:
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.
Binary Bundles and Executables
WindowsThe 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".
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..
|WebAdmin @ cs.tcd.ie|