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 Richard.Moot@labri.fr.
In addition you need the GraphViz set of graph display tools to view the graphs produced by Grail.
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.
tar xfz grail3.tgz
to extract all the necessary files from the archive. The preferred method of installation is by simply typing.
/some/directory/ is an existing directory where you
have write and execute permissions. Grail will be installed in the
Grail of this directory, whereas the executable will end up in the
bin subdirectory. The prefix defaults
Continue by typing.
to compile the Grail files. Finally, type.
to install all Grail files. Now you can start Grail by typing.
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 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 all_solutions.pl 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.
The files logarr.pl (for logarithmic access arrays) ordset.pl (for ordered sets) and the warshall/2 predicate from graph.pl 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 tree234.pl 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.