The DLV system for knowledge representation and reasoning

By Nicola Leone, Gerald Pfeifer, Wolfgang Faber, Thomas Eiter, Georg Gottlob, Simona Perri, Francesco Scarcello. TOCL, 2002

1,330 citations recorded by the source corpus.

Disjunctive Logic Programming (DLP) is an advanced formalism for knowledge representation and reasoning, which is very expressive in a precise mathematical sense: it allows one to express every property of finite structures that is decidable in the complexity class ΣP2 (NPNP). Thus, under widely believed assumptions, DLP is strictly more expressive than normal (disjunction-free) logic programming, whose expressiveness is limited to properties decidable in NP. Importantly, apart from enlarging the class of applications which can be encoded in the language, disjunction often allows for representing problems of lower complexity in a simpler and more natural fashion.This article presents the DLV system, which is widely considered the state-of-the-art implementation of disjunctive logic programming, and addresses several aspects. As for problem solving, we provide a formal definition of its kernel language, function-free disjunctive logic programs (also known as disjunctive datalog), extended by weak constraints, which are a powerful tool to express optimization problems. We then illustrate the usage of DLV as a tool for knowledge representation and reasoning, describing a new declarative programming methodology which allows one to encode complex problems (up to ΔP3-complete problems) in a declarative fashion. On the foundational side, we provide a detailed analysis of the computational complexity of the language of DLV, and by deriving new complexity results we chart a complete picture of the complexity of this language and important fragments thereof.Furthermore, we illustrate the general architecture of the DLV system, which has been influenced by these results. As for applications, we overview application front-ends which have been developed on top of DLV to solve specific knowledge representation tasks, and we briefly describe the main international projects investigating the potential of the system for industrial exploitation. Finally, we report about thorough experimentation and benchmarking, which has been carried out to assess the efficiency of the system. The experimental results confirm the solidity of DLV and highlight its potential for emerging application areas like knowledge management and information integration.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/1888bbaf6203ddfacffa4ff70f5e01a102c29895

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Conflict-driven answer set solving: From theory to practice (2012, methodology): “[119,83,15]), their performance has so far not matched the one of modern solvers for Satisfiability (SAT; [12]) checking.”
clasp : A Conflict-Driven Answer Set Solver (2007, background): “Different from smodels [8] and dlv [9], unfounded set detection within clasp does not determine greatest unfounded sets.”
Semi-stable semantics (2006, background): “…of those semantics, e.g. grounded and preferred, have become popular in the domain of formal argumentation, stable semantics still enjoys strong support in fields like (normal) logic programming and answer set programming, where various interpretations of the stable model semantics exist [40] [37].”
Multi-shot ASP solving with clingo (2017, methodology): “This view is best reflected by the input/output behavior of monolithic ASP systems like dlv (Leone et al. 2006) and (original) clingo (Gebser et al.”
Combining answer set programming with description logics for the Semantic Web (2004, positive): “On the computational side, we have realized a prototype implementation for weak answer sets, employing the description logic engine RACER (Haarslev & Möller 2001) and the answer set engine DLV (Leone et al. 2002), which is based on interleaved calls until a fixpoint is reached.”
Potassco: The Potsdam Answer Set Solving Collection (2011, neutral): “…yields: $ gringo -t beaver turing ... state(a,n,0,n). state(b,l(n,1),0,n). state(a,n,1,r(1,n)). state(c,n,0,r(1,r(1,n))). state(b,n,0,r(1,r(1,r(1,n)))). state(a,n,0,r(1,r(1,r(1,r(1,n))))). state(b,l(n,1),1,r(1,r(1,r(1,n)))). state(b,l(l(n,1),1),1,r(1,r(1,n))). state(b,l(l(l(n,1),1),1),1,r(1,n)).…”
Answer Set Solving in Practice (2012, neutral): “[52] N.”
Conflict-Driven Answer Set Solving (2007, background): “Although the corresponding solvers are highly optimized (cf. [Simons et al. , 2002; Leone et al. , 2006]), their performance does not match the one of state-of-the-art solvers for satisﬁability checking (SAT; [Mitchell, 2005]).”