GRAIL 0

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

Grail 0 is a reduced version of the unsupported Grail 2 parser. Most notably, the entire user interface has been removed and replaced by shell/Prolog commands. An important advantage of Grail 0 is that it allows the generation of natural deduction proofs.

The current version of Grail 0 is based on the source code developed by Richard Moot, Xander Schrijen and Gert Jan Verhoog.

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 currently support the generation of natural deduction output.

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 SWI Prolog 6.4.1 (or later) installed on your computer to run Grail. Porting to other Prologs should be relatively simple.

The current distribution was last modified at 23 February 2015 and has been verified to work with SWI Prolog 6.4.1.

DOCUMENTATION

The file grail/fragments/example.pl provides an empty example grammar with comments on how to modify it for your own use. Extend this file with your own lexicon and structural rules.

The man source code is the file grail/sources/grail.pl. You can start Grail as follows.
cd grail/sources
swipl
[grail].

Type grail_help. for an overview of the available commands. You can load a grammar as follows.

load_fragment('../fragments/q.pl').

You can specify the natural deduction output format as follows (here Prawitz-style natural deduction).

load_output_module(prawitz_tex).

Finally, you can parse a sentence as follows.

parseall([who,john,talks,to],rel).

This generates a LaTeX file proofs1.tex containing the natural deduction version of any proofs found.

LEXICAL ENTRIES

Lexical entries are of the form.

lex(Word, Formula, Semantics).

Where Word is a Prolog atom, Formula is a multimodal formula and Semantics is a lexical lambda term, in the formats shown below.

BACKGROUND READING

Some papers I wrote about Grail.

Richard.Moot@labri.fr