RACE Web Service

Introduction

This document describes the RACE web service. The service provides reasoning features for ACE texts. It uses SOAP 1.1 for communication and it can be accessed over the HTTP protocol using POST. The URL of the service is

http://attempto.ifi.uzh.ch/ws/race/racews.perl

There is a WSDL file that defines the interface to the web service. Furthermore, there is a web interface that relies on the web service.

The rest of this document gives a short description of how the SOAP messages have to look like, in order to be accepted by the RACE web service.

Request

A request to the RACE web service needs one single Request-element inside of the body-part of the SOAP-envelope. This element can contain the following sub-elements:

Element Name	Count	Content	Description
Axioms	1	text	The Axioms as an ACE text.
Theorems	0-1	text	The theorems, respectively the query, as an ACE text. This element must be present for the modes prove and answer_query, but is not allowed for check_consistency.
Mode	1	check_consistency \| prove \| answer_query	The mode of the reasoner. Using check_consistency, the reasoner checks whether the axioms are consistent. In the mode prove, the reasoner tries to prove the theorems on the basis of the axioms. In the mode answer_query finally, the reasoner tries to answer the query stated by Theorems on the basis of the axioms. Note that RACE uses internal auxiliary axioms for its operation.
Parameter	0-n	raw	Parameters of the reasoner. The presense of a parameter activates it. The parameter raw enables the output of all proofs together with the auxiliary axioms used during a proof.

For example, a request to check an ACE text for consistency can look like this:

<?xml version="1.0" encoding="UTF-8"?>

<env:Envelope xmlns:env="http://schemas.xmlsoap.org/soap/envelope/">
    <env:Body>
        <race:Request xmlns:race="http://attempto.ifi.uzh.ch/race">
            <race:Axioms>John is a man. Mary is a woman. John is not a man.</race:Axioms>
            <race:Mode>check_consistency</race:Mode>
        </race:Request>
    </env:Body>
</env:Envelope>

Reply

The reply of the RACE web service has a single Reply-element inside of the body-part of the SOAP-message. The sub-elements of this element depend on the request:

Element	Count	Description
Message	0-n	Warning or error message.
Runtime	1	The time that was needed to calculate the answer in milliseconds.
Proof	0-n	This contains the subset of the axioms that was used for the proof. The axioms are split into ACE axioms and auxiliary axioms.
WhyNot	0-1	In the case of an unsuccessful proof or query, this argument returns the words or phrases of the axioms that could not be proved.

For example, the request of the previous section would lead to the following reply:

<?xml version="1.0" encoding="UTF-8"?>

<env:Envelope
    xmlns:env="http://schemas.xmlsoap.org/soap/envelope/"
    xmlns:race="http://attempto.ifi.uzh.ch/race">
  <env:Body>
    <race:Reply>
      <race:Runtime>30</race:Runtime>
      <race:Proof>
        <race:UsedAxioms>
          <race:Axiom>John is not a man.</race:Axiom>
          <race:Axiom>John is a man.</race:Axiom>
        </race:UsedAxioms>
        <race:UsedAuxAxioms/>
      </race:Proof>
    </race:Reply>
  </env:Body>
</env:Envelope>

Tobias Kuhn/Norbert E. Fuchs, 2011-05-30