Downloads for project in Axiomatic Translation of Modal Logic 2007/8 Manchester.



Contents:
1. On-line interface for SPASS with Axiomatic Translation - Try the software here!!.
2. Download pre-compiled binaries of SPASS with Axiomatic Translation of Modal Logic to run on your local machine.
3. Download the web-based interface for SPASS with Axiomatic Translation to install on you local machine.
4. Download the code for SPASS with Axiomatic Translation to compile and run on you local machine.
5. For developers - download the JAVA test system for SPASS with Axiomatic Translation.
6. My dissertation is available here.
7. Any Questions?
8. Reference




1. On-line interface for SPASS with Axiomatic Translation - Try the software here!!.

MANCHESTER SERVER is back ON-LINE!

Web Interface where you can run the latest version of SPASS with Axiomatic Translation of Modal Logic on-line (with XHTML,CSS,JavaScript,Ajax, v.1.1.2) Try the software HERE!!

This on-line version of SPASS for Axiomatic Translation of Modal Logic is hosted at the University of Manchester (Dept. Computer Science), where this project is underway with Dr. Renate Schmidt. (Homepage here)

Note:This version of the SPASS interface has been designed to interact with the Firefox browser. In some cases Firefox will inappropriately cache data from an older version of the software - so if you have been using an older version, you are advised to "clear private data" in Firefox. You are recommended to use the default fonts in Firefox (a note of these is made below).

Examples of usage are available in the SC (sample scripts) tab under the Misc dropdown.

2. Download pre-compiled binaries of SPASS with Axiomatic Translation of Modal Logic to run on your local machine.

NOTE: If at all possible, you are recommended to download the latest version of the code from the link below, and compile it yourself. These binaries are only provided for the convenience of those who don't have compilers installed. (Other binaries for different versions of the software and for different operating systems can be provided on request).

The binary for Mac 10.5.1 Intel is v1.1.0 HERE.
The binary for Mac 10.3.9 PowerPC is v1.1.0 HERE.
The binary for Fedora Core Linux i386 is v1.1.0 HERE.
The binary for Windows 2000 / XP running Cygwin is v1.1.0 HERE.
The binary for Solaris 5.9 is v1.1.0 HERE.

The beta manual is HERE.

A partial set of examples is v1.1.0 HERE (56 MB; 1GB+ when uncompressed). A digest of the data is HERE in Excel format 5MB

3. Download the web-based interface for SPASS with Axiomatic Translation to install on you local machine.

The interface code v.1.1.2 is HERE (Please take note of the copyright notices included).
The interface code v.1.1.0 is HERE (Please take note of the copyright notices included).

To install & use ... download and unzip the interface. Move the directory public_html into your own root directory for the webserver. Go to the cgi-bin directory. Copy the correct binary for your system into cgi-bin (downloaded above), overwriting the pre-existing SPASS binary. Copy or link the contents of cgi-bin to your cgi-bin directory on your webserver. Finally, edit lineNumbers.cgi and spass0.cgi to reflect the location of your perl binary, and the location of your SPASS binary VIA the webserver cgi-bin. Depending on your system you may also have to delete the lines "$data =~ s/" and "//g;" from both cgi files, and if nl is not on your system, replace this call in lineNumbers.cgi with "grep -n . " ...without the quotes. You will also need to edit the line var cgiLoc = "http://www2.cs.man.ac.uk/smithk-bin/"; in spass.js in the KJSpass directory, usually to var cgiLoc = "/cgi-bin/";

4. Download the code for SPASS with Axiomatic Translation to compile and run on you local machine.

Code for v1.1.2 extensions to SPASS (in C) is HERE (Please take note of the copyright notices included in eml.c).
Code for v1.1.1 extensions to SPASS (in C) is HERE (Please take note of the copyright notices included in eml.c).
Code for v1.1.0 extensions to SPASS (in C) is HERE (Please take note of the copyright notices included in eml.c).
Code for v1.1.0 extensions to SPASS (in C) with modifications to perform the experiments described in chapter 8 of the dissertation is HERE (Please take note of the copyright notices included in eml.c).

To compile:
./configure --prefix=/Users/john/release/bin        (put your own installation directory in here!!)
make
make install

Changes since version 1.1.0:
1.1.1:
   Bug fixes in interconversion of SPASS "axioms" and "conjectures" (when 1 conjecture is used)
   Fixed Interface:incorrect link at Main/Script/More Info. Now redirects to http://project.kjsmith.net/
   Fixed handling of input formula of format and(X,X). Now interpreted as X (not and(X)).
   Modified comments in code to remove OS dependence. Logical Not now represented by !
1.1.2:
   Modified semantics of conjectures and axioms: axioms alone define global satisfiability mode; conjectures alone define local satisfiability mode; both axioms and conjectures define local satisfiability mode.
   Added flag to allow global and local satisfiablity to be chosen.
   Deleted flag allowing composition in axiom 5 to be turned off.

5. For developers - download the JAVA test system for SPASS with Axiomatic Translation.

Code for the v1.1.0 test system (in Java, compatible with Java 1.4+, 5280 tests) is HERE (Please take note of the copyright notices included in Main.java), with templates required for Java tests HERE
Jasper is provided as a NetBeans 6.1 (www.netbeans.org) project file. The tests execute from Main.Java (in the root directory of "jasper/src"). Jasper runs a comparison with the extended SPASS executable. You will need to edit jasper/src/main/Run.java to point to your executable for extended SPASS, and to the templates downloaded from the link above. The output is printed to 'standard output' and into log files in the directories logs, logs2 & logs3.

6. My dissertation is available here.

Original Paper by R.Schmidt et.al: pdf here.
MSc Presentation: Slides here. Tables here .

MSc Dissertation:
Full Document.

Subsections from the MSc Dissertation:
Titles, Abstract, etc , Introduction , Axiomatic Translation , Materials&Methods , Requirements , Specification , Implementation, Testing & Results , Results Figures, Discussion, References, Appendix

(Previous drafts of these files: Abstract , Materials&Methods , Introduction , Axiomatic Translation , Specification , Implementation , Testing & Results , Results Figures , Discussion , Appendix , References).


Advanced level MSc in Computer Science

The Degree Certificate.
The Academic Transcript (redacted for security purposes).


7. Any Questions?

For Help (please put the words "Modal Logic" in the subject) ... email contact: john@kjsmith.net (or smithk@cs.man.ac.uk)

My homepage is Here.

8. Reference

For Reference: This version of SPASS for Axiomatic Translation of Modal Logic Formulae is the first release. It is built on-top-of the latest 3.0 release of SPASS available. The original version of SPASS WITHOUT Axiomatic Translation of Modal logic is HERE.

    For Information ... In firefox, the Default Fonts are:
   
    In options...content tab...
       Times New Roman ... size 16
    In the Advanced Button ...
       For ... Western Fonts
       Proportional: Serif ... size 16
       Serif: Times New Roman
       Sans_serif: Arial
       Monospace: Courier New ... size 13
       Minimum Font Size: ... None
       Default Character Encoding: ... Western (ISO-8859-1)
       Allow pages to choose their own fonts... Yes






Downloads for project on Patterns IDE 2004/5 Birmingham (in Java).




Java Code: Here.

'Conversion' level MSc in Computer Science

Dissertation: An MDA Tool in JAVA: The Patterns IDE ... Here (45MB Scanned PDF - original text has been lost - sorry!).
Degree Certificate (redacted for security purposes).
Postgraduate Prize Certificate.
Academic Transcript (redacted for security purposes).





Miscellaneous Excersies from MSc level courses in Computer Science (under construction).





Univ. Manchester Adv. MSc - Machine Learning - Matlab exercises.
Univ. Manchester Adv. MSc - Machine Learning project.
Univ. Manchester Adv. MSc - Automated Reasoning Part 1.
Univ. Manchester Adv. MSc - Automated Reasoning Part 2.
Univ. Manchester Adv. MSc - Semistructured Data & XML.
Univ. Manchester Adv. MSc - Advanced DataBase Technologies.
Univ. Manchester Adv. MSc - Knowledge Representation & Reasoning.
.
.
.
.
.
.