DAML Logo - Link to www.DAML.org

DAML Reasoning

Home | About DAML | Announcements | Roadmap | Site Search

This page summarizes reasoning with DAML+OIL. It is a result of the Reasoning and Rules breakout session at the July 2001 DAML PI Meeting, and inspired by the previous DAML XSB page.

Send additions/updates/corrections to webmaster@daml.org.


DAML Projects Involving Reasoning

The following project summaries were submitted for the July 2001 breakout session:
Cycorp's OpenCyc for DAML ontologies will provide taxonomic inferences as described at http://opencyc.sourceforge.net/daml/daml-taxonomic-inferences.html. Cycorp has provided java bindings for its ontology navigation API that will soon be published at http://www.opencyc.org and http://www.sourceforge.net/projects/opencyc.
Lockheed Martin, VIS, Kestrel
Within the UBOT project (Lockheed Martin, VIS and Kestrel) we are working on consistency checking of DAML ontologies. We have developed a program called ConsVISor which checks whether all axioms of DAML are satisfied by a particular ontology or annotation. Additionally, we have translated DAML KIF axioms into Slang. This allowed us to perform "deeper" consistency checking of both the DAML axiomatization and of DAML ontologies and annotations. Once an ontology is translated to Slang, we can not only check its consistency, but also perform reasoning (theorem proving). More information on our efforts can be found at http://vis.home.mindspring.com.
Stanford KSL
KSL is developing technology for reasoning with knowledge expressed in DAML on distributed Web sites. We are addressing both the standard issues about how to reason effectively with knowledge expressed in an object-oriented language augmented with rules and the issues raised by the knowledge using ontologies resident on (perhaps multiple) other Web sites. The technology includes a DAML reasoner called JTP implemented in JAVA that contains a general-purpose theorem prover integrated with a collection of special-purpose reasoners designed specifically for DAML+OIL and specific task domains. See http://www.ksl.stanford.edu/projects/DAML/.
While it's more the focus of other projects rather than our DAML effort, we are doing some work with extending Mark Stickel's PTTP theorem prover to support our inference needs. We can read and do first order logic inference on a version of KIF. Since we can translate KIF to DAML and back, we expect that this software will be useful for our DAML efforts in the coming year, especially as we develop more sophisticated ontology translation methods.
UMBC has developed an environment for reasoning with information expressed in DAML to support agents which do intelligent filtering of talk announcements as part of the ITTALKS application. The ITTALKS agent sends a user's agent ACL messages notifying them of new talks or changes to earlier talks using DAML as the "content language". The user's agent reasons about the new talk to decide (1) how well it matches the user's interests, (2) if it is feasible for him to attend based on his expected location and (3) it it fits his current schedule. If the outcome is positive, the agent places an item for the talk on the user's schedule. We are also doing a more limited range of reasoning with DAML using XSB in support of service description and discovery for bluetooth agents. Our current environment uses XSB as the inference engine, YAJXB as the bridge between XSB and Java, and the RDF API as a DAML parser. More information can be found at http://daml.umbc.edu/papers/, http://daml.umbc.edu/reasoning/ and by contacting Youyong Zou.
Univerity of Manchester
The FaCT system (http://www.cs.man.ac.uk/FaCT) provides reasoning services for the SHIQ description logic via a CORBA client-server interface. A simple translation of DAML+OIL into SHIQ allows FaCT to be used as a reasoning service for DAML+OIL (a direct DAML+OIL interface is under development). By using a highly optimized implementation of a sound and complete tableaux algorithm, FaCT is able to provide reasoning services that are both efficient and effective. FaCT is used by both the OilEd (http://img.cs.man.ac.uk/oil) and Protege ontology editors to provide subsumption and consistency checking support for ontology design.
The Yale/BBN/Kestrel group is working on the problem of taking a service description from a web-based agent, and using it as the basis for planning. This raises several issues, all of which involve reasoning: (1) If the service description is in an unexpected vocabulary, how do you translate? (2) What must a service description look like in order for a planner to use it? (3) What changes to existing planners must be made for them to use these descriptions? (4) In the end, the only primitive actions you can take on the web are sending and receiving messages. How are these messages constructed and deconstructed?

Tools for Reasoning with DAML+OIL

The following
DAML+OIL tools relate to reasoning:

Other Information

$Id: index.xml,v 1.3 2002/04/11 14:46:22 kmbarber Exp $