User's Guide to Grail 2.0

Richard Moot

Table of Contents

  1. Introduction
  2. Main Window
  3. Status Window
  4. Proof Net Window
  5. Rewrite Window
  6. Lexicon Window
  7. Postulate Window
  8. Analysis Window

1. Introduction

The Grail project is an automated deduction system for multimodal categorial logics. It is developed as part of a PhD project at UiL-OTS (Utrecht, The Netherlands).

The current version is the beta release of version 2.0. It has some minor inconsistencies, and maybe even some, ahem, undocumented features.

Grail operates from a non-associative base logic, but allows you to plug in user-defined structural postulates. It operates using a combination of labeled deduction and proof nets as described in [Moortgat97], but can produce output in the more familiar natural deduction format.

2. The Main Window

The main window is your interface to the theorem prover. From here you can parse grammatical expressions, load and save grammar fragments, and open other windows to view and edit these fragments.

The window will display a list of previously parsed sentences for the current fragment, and an input section where you can enter new expressions.

Clicking on one of the sentences will display the words in the word entry section, and the goal formula in the formula entry section. You can edit the words and the formula, and parse the sentence by pressing (Enter) or the [Parse] button. Double clicking one of the sentences will parse it immediately.

When parsing, a status window will appear which gives an indication of the computations being performed, and when ready will display either `done' or `failed' depending on whether a proof was found. The [Abort] button cancels the computation when you run out of patience.

Command Buttons below the entry sections you will find the following command buttons:

Menu Bar from the menu bar of the main window, you can access the following operations:

3. The Status Window

The status window gives information about the current state of the computation, and allows you to abort time-consuming parses. It will open automatically during proof search, or you can open it by selecting [Window/Status Window] or by typing (Control-s).

The white part of the status bar gives an estimate of the number of links which have not been tried yet.

The status message can be one of the following:

Menu Bar From the menu bar, we can select the following:

4. The Proof Net Window

When the interactive debugger is on, the status window will be replaced by the proof net window. In the proof net window we see the current partial proof structure, with the decomposition trees of the formulas the current lookup assigns to the words from the sentence above the corresponding word. Positive atomic formulas drawn in white and negative atomic formulas drawn in black. Here atomic formulas of opposite polarity are linked until we find a proof structure which is both acyclic and connected.

The console buttons offer the following options

In addition, you can click on the atomic formulas themselves to have complete control over the order in which the axioms are linked. As a first step you select any atom not currently linked by an axiom link. The selected formula will then appear in a black box and the atoms of opposite polarity which have not been tried before will appear in a white box, as shown the figure above. You can then click any of the boxed formulas to perform an axiom link.

If at any time you perform a link which results in a cyclic or disconnected proof structure, you will get a message and the current link will fail.

Menu Bar For the menu bar, we can select the following:

5. The Rewrite Window

When the interactive debugger is on, you can open the rewrite window by selecting [Window/Rewrite Window] or by typing (Control-r).

The rewrite window above displays the current label and allows you to perform rewrite operations on this label. Clicking on a node of the label will cause a pop-up menu with the label conversions rooted at that node to appear. You can apply a conversion by selecting it from the menu. Any alternatives to your choice will be added to the queue.

The status message gives you an indication of the number of unvisited labels in the queue and of the current depth.

As shown in the figure, some label constructors are drawn in dark grey. These correspond to unsatisfied constraints, which are checked by the following label conversions

For the non-associative base logic, these are all available conversions. However, you can relax the constraints by specifying your own structural postulates as specified in Section 8. Each structural postulate can be applied backwards as a label conversion.

You can rewrite a label until you reach one where all constraints have been satisfied and the words are in the order required by the input sentence. Grail will only check if you meet these conditions when you press the [Creep] or [Leap] button in order to allow you to continue rewriting a label even if all constraints have been satisfied.

The console buttons offer the following options

Menu Bar For the menu bar, we can select the following:

6. The Lexicon Window

You can open the lexicon window from the menu bar in the main window by selecting [Window/Lexicon Window], or by typing (Control-l). The lexicon window displays a list of the words in the fragment and of the formulas assigned to them. From here you can edit, delete or enter new lexical entries. Clicking an entry will select it, indicated by the selection bar. The next edit or delete command will then be applied to that entry. Double-clicking one of the entries will open the edit lexical entry window, with that entry displayed in it (see Section 6.1 for more on the editing of lexical entries). Clicking one of the entries with the (Control) key depressed will delete it. Menu Bar from the menu bar of the lexicon window the following operations are available:

6.1 Editing a Lexical Entry

The edit entry window is where you modify existing entries in the lexicon or create new entries from scratch. You can open the edit entry window by selecting [Edit/New Entry] or [Edit/Edit Entry] from the lexicon window.

The edits you perform here will only be stored in the lexicon when you press (Control-s) or select [Edit/Store Entry] from the menu bar, so you don't have to worry about accidentally modifying your lexicon.

A lexical entry consists of three parts: prosodics, a syntactic formula and semantics.

Formula

The formula edit fields take up the upper section of the window.

Selection

The formula is displayed as its construction tree. You can select a part of the formula by clicking on it. The selection cursor appears as a box surrounding the root of the selected tree.

Insertion Points A special constant `*' functions as an insertion point in the formula. It is not a part of the formula language. By pressing (Control-k) the selected tree will be replaced by this constant, and copied to the paste buffer.

When an insertion point is selected (as shown in the figure above), you can insert something at that position in one of the following ways:

Prosodics

The prosodics of an entry is the way it will appear in your expressions. You can enter a Prolog term in the prosodics entry section. The current version does not support lexical entries consisting of more than one word.

Semantics

You can give your lexical entry a Montague-style meaning recipe in the semantics entry section. Editing the semantics in the current version is very cumbersome, as it requires you to type in the internal semantic representation. It is recommended you leave the semantics field empty or type in a single constant. If you really want to enter lambda term meaning recipes you can use the table below to convert lambda terms to Prolog terms.

Menu Bar In the edit lexical entry window, you can select the following from the menu bar

7. The Postulate Window

The postulate window displays the structural postulates in the current fragment. From here you can delete or edit structural postulates.

You can open the postulate window from the menu bar in the main window by selecting [Window/Postulate Window], or by typing (Control-p).

Clicking on a postulate will select it. This will cause a selection bar to appear over it, and allows you to perform the operations in the edit menu on it.

Double clicking a postulate will display that postulate in the edit postulate window.

Clicking a postulate with (Control) depressed will delete that postulate.

Pressing mouse button 2 over a postulate will change the status of the postulate from enabled to disabled or vice versa. This allows you to experiment with the effects of structural postulates without having to create several versions of the same fragment.

Menu Bar From the menu bar, the following options are available:

7.1 Editing a Postulate

Editing a postulate is much like editing a formula. There is now a formula on both the left and the right hand side of the postulate arrow. Selection and cut/copy/paste can be performed as before.

Instead of atomic formulas we now have structural variables, which can be inserted from the variable menu, and our choice of constructors is limited to and .

Postulate Arrow

By clicking on the postulate arrow it will change from to to . This makes it easier to store equivalences or inverses of postulates. In the postulate window, all postulates will appear in their left to right version regardless of the postulate arrow, so storing a postulate will in fact be the same as storing both and .

Postulate Names

You can give a postulate any name which is printable in LaTeX math mode.

Valid Postulates

The computational architecture poses some limitations on the type of postulates allowed in your fragments. Grail will report an error when you try to store postulates of the following form:
  1. There are multiple occurrences of a variable on either side of the postulate arrow.
  2. A variable occurs on only one side of the postulate arrow.
In addition, because of the backward chaining proof search strategy, a warning will be generated when a postulate has more constructors on the left hand side than on the right hand side. If you add one of these postulates to your fragment, the proof search algorithm is not guaranteed to terminate.

Menu Bar the menu bar allows you to access the following functions:

8. The Analysis Window

The analysis window is where you can improve the performance of the theorem prover by setting the parameters for early failure. This can be done either automatically or by hand.

External Modes

Sometimes you may want to prevent a mode from occurring in the output, because it is used only as a grammar internal or auxiliary mode. By default all modes will be external, but you can set modes to internal by turning off their checkbutton here.

Lazy, Transparent and Continuous Modes

Three forms of early failure are supported which apply only to structural postulates satisfying some criteria. See [Moot 96] for descriptions of these criteria. All can be detected by the program, and only the lazy reductions test is expensive to compute. When the program suspects checking for lazy reductions will take up an unreasonable amount of time, you will get a choice to set these parameters to their default, safe settings and only perform the other tests.

Menu Bar From the menu bar, the following options are available:

Bibliography

Benthem, J. van, and A. ter Meulen (eds.) Handbook of Logic and Language. Elsevier, 1997.

Danos, V. La Logique Linéaire Appliquée à l'étude de Divers Processus de Normalisation (Principalement du Lambda-Calcul). Thèse de Doctorat, Université de Paris VII, 1990.

Gabbay, D. Labeled Deductive Systems. Clarendon Press, Oxford, 1996.

Girard, J.Y. Linear Logic. Theoretical Computer Science 50, 1987, pp. 1-102.

Moortgat, M. Categorial Type Logics. Chapter 2 of the Handbook of Logic and Language, 1997.

Moot, R. Proof Nets and Labeling for Categorial Grammar Logics. MA Thesis, Utrecht University, 1996.