Grail is a modern, flexible and robust parser/automated theorem prover for multimodal categorial grammars. It is designed to allow students and researchers to design and experiment with their grammars while at the same time offer the advanced users many optional optimisation strategies.

Grail can be run either as a command line script or as an application with a graphical interface, with the possibility to follow Grail's partial parses/proof attemps interactively.

Send your comments, bug reports or feature requests to


You will need to have SWI Prolog together with SWI Prolog's XPCE user interface installed on your computer to run Grail.

In addition you need the GraphViz set of graph display tools to view the graphs produced by Grail.


Source code is provided under the GNU Lesser General Public License.

The current distribution contains the 28 June 2012 (01:11:06 CEST) release of Grail 3.2.0; it has been verified to work with SWI-Prolog version 6.0.2 for i386-darwin11.3.0 (and SWI-Prolog version 5.10.2 for i386-darwin9.8.0), though everything should work properly on not-too-ancient SWI Prolog installations and for installations on other architectures as well.


Move the Grail tarball into the directory where you want to install it and type.

tar xfz grail3.tgz

to extract all the necessary files from the archive. The preferred method of installation is by simply typing.

./configure --prefix=/some/directory/

where /some/directory/ is an existing directory where you have write and execute permissions. Grail will be installed in the subdirectory Grail of this directory, whereas the executable will end up in the bin subdirectory. The prefix defaults to /usr/local/.

Continue by typing.


to compile the Grail files. Finally, type.

make install

to install all Grail files. Now you can start Grail by typing.


or by


if your shell doesn't normally look at your installation path. Remember also that Grail will try to write its postscript files in the current working directory, so be sure to run Grail from a place where you have writing permission if you want to see the postscript output.


A short introduction to using Grail 3 can be found in the manual or by selecting [Help/About Grail 3...] from Grail's menu bar.

A more comprehensive tutorial is currently under construction.


Grail 3 is a new implementation of the Grail engine, using many of the ideas first discussed in my thesis. Notable improvements are:

An advantage of the way the subderivations are shared in the current implementation is that Grail 3 functions as Grail 2 with the extension enabled, without incurring a performance penalty because of this.

The LaTeX natural deduction output of Grail 2 is currently not supported by Grail 3.


This research was made possible by the Centre National de la Recherche Scientifique and the Institut National de Recherche en Informatique et en Automatique.

The files (for logarithmic access arrays) (for ordered sets) and the warshall/2 predicate from are modified versions of the libraries by the same name in the Public Domain DEC-10 Prolog Library. I am indebted to the authors of those packages for putting their work in the public domain. Any blame for changes and additions to their code is mine. See the individual files for changes.

The library for 2-3-4 trees is a direct adaptation of code belonging to the Mercury library, a great resource for logic/functional programs of several standard algorithms, which is available under LGPL (Mercury itself is released under GPL). I am responsible for idiosyncratic additions to this code, as well as modification of the code to use first argument indexing as much as possible, in addition to any errors this may have produced.


Moot, R. & Puite, Q. (2002), `Proof nets for the multimodal Lambek calculus', Studia Logica 71(3), 415-442.

This paper introduces the proof nets used by Grail 3.

Moot, R. (2002), Proof Nets for Linguistic Analysis, PhD thesis, Utrecht Institute of Linguistics OTS, Utrecht University (postscript, pdf).

Chapter 7 of my thesis discusses the proof nets used by Grail and their relation to other styles of proof nets, as well as proving some of the basic results. Chapter 8 of my thesis contains a first set of ideas for using these proof nets for parsing multimodal categorial grammars which were included in Grail 3.

Moot, R. (2004), Graph algorithms for improving type-logical proof search, `Proceedings of Categorial Grammars 2004', pp. 13-28, Submitted to Elsevier Science.

This paper, first presented at Categorial Grammars 2004, includes new ideas for using graph algorithms, notably the Floyd-Warshall and Kuhn-Munkres algorithm, to improve Grail's parsing performance.

Moot, R. (2007), Filtering axiom links for proof nets, in Laura Kallmeyer, Paola Monachesi, Gerald Penn and Giorgio Satta, eds, `Proccedings of Formal Grammar 2007', to appear with CSLI.

This paper, a draft of an extended version of my Formal Grammar 2007 submission, proposes two new filtering algorithms, in addition to the ones previously implemented, and evaluates their combined performance both against randomly generated sequents and sequents extracted from corpus.