GRAIL

UPDATES

Grail 2 is currently unsupported software and has not been updated to take into account changes to SICStus Prolog since version 3.5. It will probably require some work to get Grail 2 up and running. If you manage to install and run this old version, please drop me a note about the changes you had to make to the software in order to do so.

A next generation Grail theorem prover, Grail 3, has replaced Grail 2 as the current, stable and supported version of Grail. Grail 3 has a legacy mode which allows you to used your old Grail 2 grammars without any changes.

ABOUT GRAIL

The Grail system is a tool for the development and prototyping of grammar fragments for categorial logics. Grail is an automated theorem prover based on proof nets, a graph-based representation of proofs, and labeled deduction. The theorem prover is implemented in SICStus Prolog, the user interface in TclTk.

DOWNLOAD

If you want to install Grail on you home computer, feel free to do so. Source code and binaries are provided under the GNU General Public License.

You will need to have SICStus 3#5 (or later) installed on your computer to run Grail. Porting to other Prologs should be relatively simple. In addition, the user interface requires that SICStus communicates with Tcl 7.6/Tk 4.2 (or later). Porting the user interface to other Prologs will probably be a real pain.

The current distribution was last modified at 24 October 2000 and has been verified to work with SICStus 3.8.4 and Tcl/Tk 8.2. Read the release notes.

DOCUMENTATION

To help you sort out all those confusing options, read the fine manual.

BACKGROUND READING

Some papers I wrote about Grail.

Richard.Moot@labri.fr