dlvhex

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 using git at github.com/hexhex. Packages (tarballs) of dlvhex can be downloaded from the SourceForge dlvhex project page. The latest release of the software runs on Linux-based systems and (Mac) OS X, recent development versions are also compatible with Microsoft Windows. For some systems we provide pre-built packages, for others you may build the software from source.

Please also visit our Facebook page.

If you are looking for the RDF-plugin, please have a look at the SourceForge dlvhex-semweb project page.

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.

For recent updates, please visit our News page.

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$

 

dlvhex source code @ github.com
Action Plugin
DecisionDiagrams Plugin
Description Logics Plugin
Description Logics Lite Plugin
MELD: Belief Merging Plugin
Nested HEX Plugin
MCSIE Plugin
String Plugin
dlvhex-semweb Project
Description-Of-A-Project

Documentation:
README
doxygen
Writing Plugins in C++
Writing Plugins in Python