The dlvhex system is a logic-programming reasoner for computing the models of so-called HEX-programs, which are an extension of answer-set programs towards integration of external computation sources.

For a quick overview, some examples and the possibility to evaluate HEX-programs directly in your browser, please check out the online demo. However, the system can also be installed locally.

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, (Mac) OS X, and 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.

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.


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.).



dlvhex source code @ github.com

Popular Plugins
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

Writing Plugins in C++
Writing Plugins in Python