10 Sep 2003 | NICOLA LEONE and GERALD PFEIFER and WOLFGANG FABER and THOMAS EITER and GEORG GOTTLOB and SIMONA PERRI and FRANCESCO SCARCELLO
The paper presents the DLV system, a state-of-the-art implementation of Disjunctive Logic Programming (DLP), which is a powerful formalism for knowledge representation and reasoning. DLP is expressive in a precise mathematical sense, allowing the representation of every property of finite structures decidable in the complexity class $\Sigma_2^P$ (NP$^P$). The paper provides a formal definition of the core language of DLV, which includes disjunctive logic programs extended by weak constraints. It illustrates the usage of DLV for knowledge representation and reasoning through a declarative "Guess/Check/Optimize" (GCO) programming methodology, which allows encoding complex queries and problems in a declarative manner. The paper also analyzes the computational complexity of the DLV language, deriving new complexity results and identifying syntactic subclasses with lower complexity. Additionally, it surveys application front-ends developed on top of DLV and describes international projects investigating industrial exploitation. The paper includes a detailed architecture overview, implementation techniques, and extensive experimental results comparing DLV with other systems, highlighting its efficiency and applicability to various domains.The paper presents the DLV system, a state-of-the-art implementation of Disjunctive Logic Programming (DLP), which is a powerful formalism for knowledge representation and reasoning. DLP is expressive in a precise mathematical sense, allowing the representation of every property of finite structures decidable in the complexity class $\Sigma_2^P$ (NP$^P$). The paper provides a formal definition of the core language of DLV, which includes disjunctive logic programs extended by weak constraints. It illustrates the usage of DLV for knowledge representation and reasoning through a declarative "Guess/Check/Optimize" (GCO) programming methodology, which allows encoding complex queries and problems in a declarative manner. The paper also analyzes the computational complexity of the DLV language, deriving new complexity results and identifying syntactic subclasses with lower complexity. Additionally, it surveys application front-ends developed on top of DLV and describes international projects investigating industrial exploitation. The paper includes a detailed architecture overview, implementation techniques, and extensive experimental results comparing DLV with other systems, highlighting its efficiency and applicability to various domains.