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