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.
Grail 2 is currently unsupported software. Grail 0, a
a reduced version of the Grail 2
parser, without the user interface, can be found here. Grail 0 is recommended for users primarily
interested in the natural deduction proofs generated by Grail.
For all other users, 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. Grail 3 does not
support natural deduction output.
ABOUT GRAIL 2
The Grail 2 theorem prover is implemented in SICStus Prolog, the user
interface in TclTk.
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
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.
To help you sort out all those confusing options, read the fine manual.
Some papers I wrote about Grail.
- Moot, R. (2001), A short introduction to Grail, in C. Areces & M. de Rijke, eds, `Proceedings of Methods for Modalities 2' (postscript, pdf).
- Moot, R. (1999), Grail: an
Interactive Parser for Categorial Grammars, in Proceedings of
VEXTAL'99, R. Delmonte, ed., University Ca' Foscari, Venice, pp. 255-261 (postscript, pdf).
- Moot, R. (1998), Grail: an
Automated Proof Assistant for Categorial Grammar Logics, in Proceedings of the Workshop on User Interfaces
for Theorem Provers 1998, R. Backhouse, ed., Computing Science
Report 98-08, Department of Mathematics and Computing Science, Eindhoven
University of Technology, pp. 120-129 (postscript, pdf).