A technical report published by the Knowledge Systems Laboratory at Stanford University proposes a "Proof Markup Language (PML) which "provides an interlingua for capturing the information agents need to understand results and to justify why they should believe the results." The model and tools are predicated upon a conviction that successful inter-operation between components in non-trivial Web Services transactions is dependent upon those components having a shared understanding of the results that have passed between. "In order for Semantic Web services to explain their results, they need to be able to generate justifications of their results in an exchangeable, combinable format. PML addresses the issue of understanding and trusting results generated by web services. PML classes are OWL classes, and thus are subclasses of owl:Class. They are used to build OWL documents representing both proofs and proof provenance information. PML concepts therefore can be considered to be either proof level concepts or provenance level concepts." The report provides an overview of related work and introduces an Inference Web infrastructure that uses PML as the foundation for providing explanations of web services to end users.

Bibliographic Information

A Proof Markup Language for Semantic Web Services. By Paulo Pinheiro da Silva, Deborah L. McGuinness, and Richard E. Fikes. Technical Report KSL-04-01. Knowledge Systems Laboratory, Stanford University. 2004. 20 pages, with 16 references. Abstract.

Paper Abstract

"Web services propose that they provide the means for remote interoperable access of components and software systems. However, successful inter-operation between components that do anything more than the simplest information retrieval is dependent upon those components having a shared understanding of the results that have passed between them. In this paper, we address the issue of understanding and trusting results generated by web services. We introduce a proof markup language (PML) that provides an interlingua for capturing the information agents need to understand results and to justify why they should believe the results. We also introduce our Inference Web infrastructure that uses PML as the foundation for providing explanations of web services to end users. We additionally show how PML is critical for and provides the foundation for hybrid reasoning. Our contributions in this paper focus on technological foundations for capturing formal representations of term meaning and justification descriptions thereby facilitating trust and reuse of answers from web agents."

PML Summary

"In order to provide the foundation for proof manipulations - presentations, abstractions, summaries, transformations, and explanations - we introduce a proof markup language as a proof representation interlingua. This article introduces the Proof Markup Language (PML) that can be used as follows:

• To represent different kinds of proofs ranging from formal natural deduction derivations to proof traces typically produced by highly optimized theorem provers. These representations are aimed at services that leverage inference.
• To represent proofs resulting from services aimed at information retrieval or entity extraction. These proofs may provide information concerning sources and extractors use.
• To represent different kinds of explanations varying from summaries of assertions or knowledge sources used to derive an answer to a more elaborate abstraction of a derivation path.
• To support the exchange of proof information among automated reasoners in hybrid reasoning systems.

PML classes are OWL classes; thus they are subclasses of owl:Class. They are used to build OWL documents representing both proofs and proof provenance information. Thus, PML concepts can be considered to be either proof level concepts or provenance level concepts. Primitive types mentioned in the article are from the XML schema specification1. PML documents published on the Web become a portion of the Inference Web data used when browsing and summarization tools are presenting explanations, summaries, and other viewing options to users. Inference Web also processes the PML documents to identify when portions of them may be combined to form more complex conclusions. IW also uses rewrite rules to transform the proofs into more understandable explanations. The IW data includes the PML proofs and explanations along with a registry of information used for proof presentation. The registry, called IWBase, is a distributed repository of meta-data including sources, inference engines and inference rules. This information is used to provide follow-up information concerning the elements presented in proofs and explanations.

We have developed an object-oriented modular architecture for hybrid reasoning (called the JTP architecture), a library of general-purpose reasoning system components (called the JTP library) that supports rapid development of reasoners and reasoning systems using the JTP architecture, and a multi-use reasoning system (called the JTP system) employing the JTP architecture and library. The JTP architecture and library is intended to enable the rapid building, specializing, and extending of hybrid reasoning systems. Each reasoner in a JTP hybrid reasoning system can embody special-purpose algorithms that reason more efficiently about particular commonly-occurring kinds of information. In addition, each reasoner can store and maintain some of the system's knowledge, using its own specialized representations that support faster inference about the particular kinds of information for which it is specialized. Proofs represented in PML play a central role in the JTP architecture in that they are used to represent both queries and reasoning results as they are sent to and received from reasoners during the hybrid reasoning process.

Most external representations of proofs in use by more than one automated reasoning were developed within the context of hybrid reasoning systems and logical frameworks. But even in the context of hybrid reasoning systems, few are the eorts to create a general representation of proofs rather than a representation that is able to conciliate few reasoner-specific representations. PDS [A Three-Dimensional Data Structure for Proof Plans] is an example of a general representation of proofs that is used on hybrid reasoning systems such as MBase. PML and PDS share the ability of representing proofs at different levels of abstraction. For instance, the PML ability to generate explanations from proofs corresponds to the PDS notion of 'third dimension' for is proof representation. The MBase use of PDS is also of particular interest for the PML since it demonstrated the need of a web artifact to represent proofs. Indeed, MBase uses an XML version of PDS...

We have provided a few example web services that use PML proofs. The KSL Wine Agent, the DAML Query Language Client, and the OWL Query Language Client all use PML proofs in order to provide interoperable explanations of their answers. The IWBrowser is a web service that renders PML proofs and presents them in multiple formats for humans. All of these agent's use the Stanford JTP hybrid reasoner but we are extending SRI's SNARK theorem prover10 to produce portable proofs and simultaneously integrating ISI's Prometheus query planner with Inference web. We are also pursuing discussions with designers of other reasoning systems including W3C's CWM, UT's KM, and SRI's SPARK (SRI Procedural Agent Realization Kit)."

PML is used to support web services inter-operation and trust. It has been integrated into the Inference Web infrastructure and is used as the interlingua that allows IW to present, combine, summarize, abstract, and explain answers generated by web services. PML supports hybrid reasoning and provided one implemented example of how the integration with a reasoner works. PML provides the representational foundation and Inference Web provides the tools and infrastructural support for enabling proof annotation, knowledge provenance presentation, and explanation browsing for agents and humans. This work provides the foundation from which web services may realize their promise of providing remote, interoperable access across components of distributed software systems..." [adapted from the paper]

About KSL

The Knowledge Systems Lab (KSL) conducts research in the core Artificial Intelligence areas of knowledge representation and reasoning, within the Department of Computer Science at Stanford University. Current work focuses on design and development of knowledge servers; multi-use ontologies, knowledge bases and knowledge system modules; computational environments for modeling the structure, behavior and functionality of physical devices; compositional modeling; architectures for adaptive intelligent systems; and knowledge-based systems for science, engineering and defense applications..."