How To Abstract a Proof

About this example:

This document illustrates how the Inference Web can provide infrastructure for explaining Semantic Web reasoning tasks. The document is organized as follows: a typical Semantic Web problem along with a query for solving the problem are presented; a proof describing inference steps used to derive an answer for the proposed query is presented; a proof transformation completes the process of explaining reasoning tasks in the Inference Web. Nevertheless, both the proof and its explanation are portable, sharable, interoperable and combinable since they are dumped as Inference Web proof fragments.

Problem Definition:

Determination the type of a concept or instance is a typical problem on the Semantic Web. A reasoner may ask either about the type of an object and may also ask if an object is of a particular type. Thus, lets assume that the following ontology is loaded in an inference engine:

DAML Knowledge Base (KB):

<rdf:RDF
    xmlns:rdf ="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#">
 
    <rdf:Description rdf:ID="TonysSoftShell">     
        <rdf:type rdf:resource="#CRAB"/>  
    </rdf:Description>   
 
    <rdfs:Class rdf:ID="CRAB">     
        <rdfs:subClassOf rdf:resource="#SHELLFISH"/>  
    </rdfs:Class>   
 
    <rdfs:Class rdf:ID="SHELLFISH">
        <rdfs:subClassOf rdf:resource="#SEAFOOD"/>
    </rdfs:Class>
 
</rdf:RDF>

Query:

Moreover, lets assume that the following query is submitted to a selected inference engine:

(rdf:type TonysSoftShell ?)

Query Explanations:

A query may have none, one or many answers. The (rdf:type TonysSoftShell ?) query should have more than one answer since we can anticipate in our tiny example that TonysSoftShell is both a CRAB and a SEAFOOD, for instance. Thus, an explanation is required for each answer.
Lets see how we can get an explanation for the fact that (rdf:type TonysSoftShell SEAFOOD) using the Inference Web.

A proof based on inference rules

Proofs as used in the proof-theoretical framework and based on DAML+OIL can describe reasoning tasks performed in the Semantic Web. In the following screen shot we can see a typical proof dumped by an inference engine. There, each inference step is an application of an inference rule. Axioms in proofs are either assertions from ontologies or assumptions. Some axioms are from specialized ontologies providing semantic context for inference engines.


[click here to browse this proof]

The proof itself is a combination of Atomic Proof Fragment Sets (APFSs) as described in Pinheiro da Silva and McGuinness, 2003. Humans can visualize proof fragments using the IW Browser. Artificial agents, however, may access the proofs directly. For instance, the following proof is a combination of the APFSs available in the TonysSoftShell URL (in this case, the DAML files that are presented once the link is selected). Both core elements of proofs such as APFSs and complementary elements such as ontologies are documented in the Inference Web registry. Agents can access the registry directly. The IW Registrar is responsible for handling the IW Registry. Humans may browse the registry through the Registrar.

Semantic tactics

Although essential for automated reasoning, inference rules are often inappropriate for "explaining" reasoning tasks. In fact, proofs can be explained in a more abstract and easy way when they do not mention rules. For example, the following paragraph is an explanation for the proof above.

Therefore, a mechanism is required for abstracting rules. The Inference Web relies on semantic tactics for abstracting rules (and consequently transforming proofs into explanations). Indeed, semantic tactics are proof fragments based on inference rules and semantic context axioms.

The following proof fragment presents the SuperClassInst tactic used later in our example to transform the proof into an explanation.


[Click here to browse this tactic]

Considering that proofs are based on inference rules and semantic context axioms, they can be inspected for APFSs matching the patterns of semantic tactics as illustrated in the following screen shot. Thus, the two inference steps based on the GMP inference rule and a semantic axiom (the steps marked by the red line) where replaced by the SuperClassInst semantic tactic presented above using the following substitutions: {Tony/?inst}, {CRAB/?sub} and {SEAFOOD/?super}.



An explanation based on semantic tactics

An explanation is produced as the final result of replacing inference steps based on rules by inference steps based on semantic tactics. The following screen shot is an example of how the original proof could be transformed into an explanation. For instance, the proof in English presented above can automatically be generated if templates in English are provided for semantic tactics.


[Click here to browse this explanation]

Both proofs and their explanations are combinations of APFS and they share some similar elements such as ontologies. Furthermore, elements specific to proofs, i.e., inference rules, and specific to explanations, i.e., semantic tactics, are also supported by the Inference Web. Therefore, the Inference Web is an infrastructure for handling proofs for generic purposes such as debugging inference engines, storing intermediate results of multiple tasks, etc. In particular, the Inference Web is an infrastructure for developing explanations from proofs as described in this document.