Help for TLG Theorem Prover

Help Directory

• Submitting Queries
• Display Options
• Lexicon Window
• Saving Results
• Customizing the Environment
• Getting the Most Out of the Parser

Submitting Queries [back to Directory]

Input can be typed in or selected from a corpus. The source for input is chosen with the radio buttons to the left of the input prompts.

Selecting Queries

1. Depress the radio button to the left of the Select: prompt.
2. Select input string by clicking (use the scroll bars or cursor to view all input).
3. Click on the Parse String button to submit query.

Inputting Queries

1. Depress the radio button to the left of the Input: prompt.
2. Select input field by clicking in the field.
3. Type input (use the cursor to scroll to text beyond the window).
4. Click on the Parse String button to submit query.

Resetting Input

The Reset Input button clears the input and returns selection to initial setting.

Display Options [back to Directory]

Resizing Windows

The Query window, the lexicon window, and the output display windows can be resized, but not repositioned. To resize them, simply position the cursor on their border and click to grab and drag.

Options Dialogue

Clicking on the Options button summons a dialogue box which can be used to select various options relating to the input and output of the system.

The Lexicon Window [back to Directory]

The complete list of words recognized by the parser can be browsed by scrolling in the Lexicon window. The white space between entries is an artificat of Netscape's windowing (as of version 2.0b6a).

Saving Results [back to Directory]

Results of any analysis can be saved by selecting the 'Save As' or 'Save Frame As' options, depending on whether or not you are using the frame-based browser. As of Netscape 2.0b6a, the frame currently selected is outlined in black. The results will be saved as an HTML-formatted document.

Customizing the Environment [back to Directory]

The user can reconfigure the parser's style and look by clicking on the Options button and making selections from the window that is subsequently brought up. The current options are:

Output Style

Allows the user to select the form of output. Options available are:

• Prawitz
• Fitch
• Text

Prawitz is the standard notation for natural deduction proofs in tree format. Text style approximates the Prawitz style using indentation rather than HTML tables. Fitch style presents proofs in a column, with one step per row. In this format, we indicate the string associated with each step.

Output Target

The user may select to have output displayed in the output frame of the primary parser window, in a new window for each parse, or in a single external window, depending on the choice of:

• Local Frame
• New Window
• Single External Window

Parse as

Allows the user to select which category the input string should be parsed as. Options available are:

• Any
• Finite S
• Noun Phrase

Expand Meanings

Choosing Yes or No determines whether or not the meaning postulates associated with non-logical constants are expanded.

Normalize Lambda Terms

Choosing Yes or No determines whether or not the lambda terms involved in meanings are converted to beta-eta normal form or whether they are left unreduced.

Clicking on the OK button submits the options selected and returns the user to the query frame. The Defaults button reverts all selections to their default values.

Getting the Most out of the Parser [back to Directory]

The operating system under which the server is operating (the Andrew File System at CMU) is set up to cache programs that have been recently run. As a result, the first call to the parser may be much slower than subsequent calls because of the need for my local machine to fetch a copy of SICStus Prolog to local memory.

For those with small monitors, it may help to pull down the Options menu and hide all of the buttons, captions, sites, and other clutter that occupies the top portion of most browsers.