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.



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 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.


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


Some papers I wrote about Grail.