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

Richard.Moot@labri.fr