The dlvhex Solver
dlvhex is the name of a prototype application for computing the models of so-called HEX-programs, which are an extension of Answer-Set Programs towards integration of external computation sources.
The source code of dlvhex is hosted at SourceForge. If you are looking for the RDF- or SPARQL-plugin, please have a look at the dlvhex-semweb project page. dlvhex can be obtained from the Download section.
A Brief History
At the beginning of this project, we were pondering about how to contribute to the current efforts of shaping the Semantic Web. People seem to have agreed on the Ontology Layer with OWL as its prominent specification language. The next step is to add rules in order to have powerful and sophisticated inference mechanisms on top of ontologies. This is were we saw the opportunity of introducing Answer Set Programming (ASP) to the Semantic Web development—believing in the benefits of a fully declarative and nonmonotonic logic programming semantics.
Our first goal was to extend ASP towards an interface to Description Logics, which are the theoretical foundation of ontology languages like OWL. We developed so called dl-programs, which allow for a bidirectional flow of information between an answer-set program and a DL knowledge base by a novel type of atoms.
HEX-Programs
Motivated by the need to interoperate with a broader set of external computation sources and the observation, that for meta-reasoning in the context of the Semantic Web, no adequate support is available in ASP to date, we extended the dl-program approach to HEX-programs, that is, higher-order logic programs (which accommodate meta-reasoning through higher-order atoms) with external atoms for software interoperability. Intuitively, a higher-order atom allows to quantify values over predicate names, and to freely exchange predicate symbols with constant symbols, like in the rule
C(X) :- subClassOf(D,C), D(X).
An external atom facilitates to determine the truth value of an atom through an external source of computation. For instance, the rule
reached(X) :- &reach[edge,a](X)
computes the predicate reached taking values from the predicate &reach, which computes via &reach[edge, a] all the reachable nodes in the graph edge from node a, delegating this task to an external computation source (e.g., an external deduction system, an execution library, etc.).
$Id: index.html 3651 2012-03-12 11:26:39Z peterschueller $
