Proof Markup Language (PML) Primer

KSL Working Draft 28 November 2005

This version:

http://iw.stanford.edu/doc/WD/2005/pml-primer-20051128.htm

Latest version:

http://iw.stanford.edu/doc/TR/pml-primer

Editors:

Deborah L. McGuinness (Stanford University ) dlm@ksl.stanford.edu

Paulo Pinheiro da Silva  (Stanford University) pp@ksl.stanford.edu

Li Ding (University of Maryland Baltimore County) dingli1@umbc.edu

Copyright ©2005 Stanford University Knowledge Systems, Artificial Intelligence Laboratory.

Abstract
This document provides a brief introduction to the Proof Markup Language (PML), which is part of the Inference Web (IW) infrastructure for explanations. PML was designed to function as a proof interlingua. It can be used to encode justification collections in a declarative and interoperable format. PML may be used to support applications that need to interoperate and provide access information to components that require justifications for answers. PML has been used in a number of government and corporate projects to encode justification collections. Users and agents can benefit of justification collections encoded in PML by using the Inference Web framework. IW provides a number of web tools and off-line tools for browsing, manipulating, checking, searching, combining, summarizing and rendering PML. When employing engines to generate PML, users may use the framework to validate PML encodings. This document introduces PML by motivating its need through use of simple examples. The examples are functional and can be reused to test IW tools.

Introduction

The Proof Markup Language consists of a specification of terms for encoding collections of justifications to answers in question answering scenarios. Some applications will view each justification in the collections as a formal proof and others may view each justification as an information manipulation trace describing both a reasoning process and provenance information that led a system to make a conclusion.

With PML, collections of justifications can be encoded in the interlingua, and then be shared for interoperation and information integration among heterogeneous distributed applications especially for question answering systems.

Motivating Example

Many applications work in settings where answers will not be trusted or used unless they can provide at least one justification that supports the answer that end users (people or programs) can inspect. Consider the following example:

Question & Query

John is visiting Stanford and is aware of an online tour guide agent that has information about local restaurants. John is aware of a seafood restaurant nearby called Tony's, so he asks a question in English.

 What type of food is Tony's specialty?

Upon receiving the question, the agent translated it into an internal representation, i.e. a Knowledge Interchange Format (KIF) query:

 (type TonysSpecialty ?x) 

Answer

Then the agent will run a question-answering process and come up with an answer in KIF.

 (type TonysSpecialty ShellFish) 

It then translate the answer above into English and present that to the end user.

Tony's specialty is Shellfish.

Justification Collection

Upon John's request for justifying the answer, the agent can provide a justification collection where the answer is the final conclusion of the collection. The collection may consist of one or more justifications and is encoded in PML. We use justification collections to encode justifications because one answer may have many justifications depending, for example, on the variety of information sources and the agent's run-time inference processes. In this scenario, we will first show two representative types of justification collections where only only one justification can be extracted for the the final conclusion.

• The justification for the answer says that the answer was directly asserted from some source. In this case, the answer has been directly asserted from a publication named Stanford's Tony's Specialty Example, where the conclusion "Tony's specialty is shellfish" is mentioned in KIF.

• The justification for the answer says that it was derived. In this case, the answer has been derived by Stanford's Java Theorem Prover (JTP) using one step General-Modus-Ponens inference based on two statements:
  • "Crab is subclass of Shellfish". This statement is included in an ontology named Stanford's Tony's Specialty Ontology, which mentioned the fact that crab is sub-class of shellfish in KIF.
  • "Tony's specialty is also ?x if Crab is subClassOf ?x" told by Deborah, who is a person.

Using PML to Encode Justification Collections

The justification collection for an answer is a directed acyclic graph of node sets connected by inference steps. Each node set has a conclusion and any number of inference steps including zero. An inference step is an application of an inference rule on the the conclusions of other node sets, which are called the immediate antecedents of the step. The conclusion of the node set hosting an inference step is the conclusion of applying the inference rule of the step on the immediate antecedents of the step.

A justification collection can encode one or more justifications for a given answer. The answer is the final conclusion of a collection, which is the conclusion of the node set that is not an antecedent of any inference step in the collection. A collection is said to have a single justification for the answer if every node set in the collection has exactly one inference step. If every node set in the collection has at least one inference step and ate at least one node set in the collection has two or more inference step, it is said that the collection has alternative justifications for the answer.

We will first discuss how to use PML to encode justification collections with a single justification for the answer. Then we will explain how to encode justification collections with alternative justifications for the answer. Finally, we will describe how to encode information about the query and possible question originating the answer justified by the collection.

Encoding Collections With A Single Justification for the Answer

In this section we discuss multiple ways of encoding single justifications for the answer in our scenarion. We first present a way of encoding a trivial justification for the answer and then we present a more complex justification for the same answer.

Answer Justified by a Direct Assertion

In what follows, we show how to represent justification collections for the conclusion '(type TonysSpecialty SHELLFISH)' that have been directly asserted. We have created several justification collections supporting the same conclusion with increasing amounts of provenance information.

A short justification

The justification means:

The justification can be encoded in the following PML: (browse it in IWBrowser).

NOTE: the font colors in the gray boxes are used in the following manner: (i) black for new content; (ii) red for highlighted new content; and (iii) green for visited content.

One of the most basic elements in PML is a NodeSet. A NodeSet is used to encode information about an information manipulation process that was used to derive a conclusion.

This example shows a simple instance of NodeSet which captures one justification for information that has been directly asserted. A NodeSet usually has the following properties:

• " hasConclusion: the conclusion of the direct assertion.
• " hasLanguage: the URI of the metadata about the language encoding the conclusion.
• " isConsequentOf: the InferenceStep used to obtain the conclusion

An instance of InferenceStep encodes one justification for the conclusion of NodeSet. It usually has the following properties:

• " hasIndex: auxiliary property for sorting the inference step since a node set may be justified by multiple inference steps independently.
• " hasRule: the URI of the metadata about the Rule used to derive the conclusion. In this case, "Told" refers to a direct assertion. The conclusion of a told inference step is a statement in the knowledge base.

A refinement of the above justification (with source usage information)

The justification means:

The justification can be encoded in the following PML: (browse it in IWBrowser)

This example expands the example above by adding additional source information. The PML utilizes the SourceUsage construct. An instance of SourceUsage caputures the source and how the source has been used, and it usually has the following properties:

• usageTime: this property records the time when this source has been accessed to draw the conclusion. PML uses a standard XML schema datatype format to encode time (xsd:dateTime).
• hasSource: the URI of the metadata of the registered source. In this example, it is the Stanford's Tony's Specialty Example.

A refinement of the above justification (with enriched source usage information)

The justification means:

The justification can be encoded in the following PML: (browse it in IWBrowser)

This example includes additional information using SourceUsage. It specifies the portion of the source text being used. These two properties are not required since they are auxiliary and often used for display purposes.

Answer Justified as an Inference Result

In what follows, we show how to represent justifications derived from inference. A very simple justification with three node sets are elaborated below. We will quickly mention representing the premises and elaborate the construction

The premises (from direct assertion)

Premise 1:

The justification can be encoded in the following PML: (browse it in IWBrowser)

Premise 2:

The justification can be encoded in the following PML: (browse it in IWBrowser)

A simple derived justification

The justification means:

The justification can be encoded in the following PML: (browse it in IWBrowser)

The derived justification differs from direct assertion in that (i) it uses uses rules other than Direct Assertion and (ii) it specifies addition information including:

• hasAntecedent: the URI of the NodeSet which serves as premise.

A refinement of the above justification (with inference engine specified)

The justification means:

The justification can be encoded in the following PML: (browse it in IWBrowser)

• hasInferenceEngine: the URI of metadata of the inference engine used to derive this proof

A refinement of the above justification (with variable mapping specified)

The justification means:

The justification can be encoded in the following PML: (browse it in IWBrowser)

PML also enable us to preserve the generic conclusion with associated Variable Mapping. An instance of Mapping records the variable bindings obtained in inference, and the conclusion does not have to be grounded. The semantics of the conclusion is in fact the one after variable mappings have been applied.

Encoding Answer with Multiple Justifications

A NodeSet may contain two inference steps, which lead to two alternative justifications of the same conclusion.

The justification means:

The justification can be encoded in the following PML: (browse it in IWBrowser)

Encoding Proofs

Encoding the Question

An instance of question records the original user's question, which is an English sentence in this scenario.

The question is represented in PML as below:

Encoding the Query/Answer

An instance of query records the translated internal representation of user's question, which is a KIF query in this scenario.

The query is represented in PML as below: (browse it in IWBrowser)

In this query, we need to specify the following information that captures how the query has been answered.

• "queryContent" encodes the internal representation of the query
• "isFromEngine" links to metadata of inference engine that generates the justification.
• "isQueryFor" links to the original question that generates this query
• "hasAnswer" links to the root nodesets of the jusification collections

Linking NodeSets to Query and Answer

• "fromQuery": PML supports links from the NodeSet encoding the final conclusion of a justification collection to an query

• "fromAnswer": PML supports links from other NodeSets in a justification collection to the NodeSet encoding the final conclusion

References

All references are available from the Inference Web publication page: http://iw.stanford.edu/documents_papers.html

Best PML reference:
Paulo Pinheiro da Silva, Deborah L. McGuinness and Richard Fikes. A Proof Markup Language for Semantic Web Services Information Systems http://www.ksl.stanford.edu/KSL_Abstracts/KSL-04-01.html

Best Inference Web reference:
Deborah L. McGuinness and Paulo Pinheiro da Silva. Explaining Answers from the Semantic Web: The Inference Web Approach Journal of Web Semantics Vol.1 No.4., pages 397-413, October 2004. http://www.ksl.stanford.edu/KSL_Abstracts/KSL-04-03.html