RACE Web Client Help

The Attempto Reasoner RACE provides you with three deduction modes:

• check the consistency of ACE axioms
• show that ACE theorems can be deduced from ACE axioms
• answer ACE queries from ACE axioms

This document describes the web client of RACE. The web client is a front-end to the RACE web service. Read the RACE Web Service documentation to learn how to use RACE directly from your applications.

You can find information on Attempto Controlled English (ACE) in the documents ACE in a Nutshell, ACE Construction Rules, ACE Interpretation Rules, and ACE Troubleshooting Guide. Check also the Attempto publications.

User Interface: Input

At the beginning the RACE web client offers you the following graphical user interface.

Buttons have tool-tips. In order to see them, hover the mouse over the corresponding button.

The following describes the graphical user interface in more detail.

• The Show Parameters button opens the Parameter window that allows you to set the parameters of RACE (see below).
• The Show Help button opens this help text.
• The Axioms text field must contain either an ACE text or its web address (URL).
• The tabs Check Consistency, Prove and Answer Query allow you to select one of the three deduction modes of RACE.
• Selecting the tab Check Consistency reveals a button Check Consistency. Clicking this button checks the consistency of the ACE text previously entered in the Axioms text field.
• Selecting the tab Prove reveals a text field Theorems and a button Prove. Clicking this button checks whether the ACE text entered in Theorems logically follows from the ACE text entered in Axioms.
• Selecting the tab Answer Query reveals a text field Query and a button Answer Query. Clicking this button checks whether the ACE query entered in Query can be answered from the ACE text entered in Axioms.

Parameters

Per default RACE shows all minimal proofs, i.e. all minimal sets of inconsistent axioms, all minimal sets of axioms to prove a theorem, or all minimal sets of axioms to answer a query. In reality, RACE also generates non-minimal proofs and uses internal auxiliary axioms. One parameter allows you to output all raw proofs, i.e. all minimal proofs and all non-minimal proofs together with the auxiliary axioms used during the proofs. This parameter is mainly intended for testing.

• enable the output of all raw proofs (raw); default: not set

User Interface: Output

Each of the three deduction modes of RACE generates its specific output. The web interface preserves the complete output of each deduction so that you can keep track of what you did, and if necessary easily return to a previous deduction.

Output of Consistency Checking

The output displays the overall time including the time used for network transmissions, and separately the time RACE used for the consistency check.

Then the output shows the axioms and the selected parameters.

If the axioms are consistent then ...

... there is the message "Axioms are consistent."

If the axioms are inconsistent then ...

... there is the message "Axioms are inconsistent. The following minimal subsets of the axioms cause inconsistency:", followed by one or more minimal inconsistent subsets of the axioms.

Output of Proofs

The output displays the overall time including the time used for network transmissions, and separately the time RACE used for the proof.

Then the output shows the axioms, the theorems and the selected parameters.

Finally the output returns the results of the proof consisting of the message "The following minimal subsets of the axioms entail the theorems:", and one or more minimal subsets of the axioms that entail the theorems.

For the case that the proof failed, see the section "Why Not?".

Output of Query Answering

The output displays the overall time including the time used for network transmissions, and separately the time RACE used to answer the query.

Then the output shows the axioms, the query and the selected parameters.

Finally the output returns the results of the deduction consisting of the message "The following minimal subsets of the axioms answer the query:", and one or more minimal subsets of the axioms that answer the query.

For the case that the query could not be answered, see the section "Why Not?".

Why Not?

If theorems cannot be proved from the axioms, respectively if a query cannot be answered by the axioms, then the output consists of the message "Theorems do not follow from axioms.", respectively the message "Query cannot be answered.", followed by a list of those parts of the theorem, respectively query, that could not be proved.

Currently this list consists of words plus their word classes, later the list will consist of real parts of the theorems, respectively query.

Output of All Raw Proofs

If you set the parameter output of all raw proofs (raw) then the output will show the results of all minimal and non-minimal deductions together with the internal auxiliary axioms used for the respective deduction. Note that the results may differ only in the auxiliary axioms being used, but not in the ACE axioms.

Switching off the parameter output of all raw proofs (raw) will again compact the results to the minimal ones, and omit the auxiliary axioms.

Error Messages

If there are errors during the parsing of ACE axioms and ACE theorems, or if RACE itself detects problems, then the output will contain error and warning messages indicating what went wrong, and suggesting how you can remove the causes of the problems.