Skip to Main content Skip to Navigation

Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs

Frédéric Besson 1 Thomas Jensen 1 Tiphaine Turpin 1 
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We present the semantic foundations for computing the least fix-point semantics of definite logic programs using only standard operations over boolean functions. More precisely, we propose a representation of sets of first-order terms by boolean functions and a provably sound formulation of intersection, union, and projection (an operation similar to restriction in relational databases) using conjunction, disjunction, and existential quantification. We report on a prototype implementation of a logic solver using Binary Decision Diagrams (BDDs) to represent boolean functions and compute the above-mentioned three operations. This work paves the way for efficient solvers for particular classes of logic programs e.g., static program analyses, which leverage BDD technologies to factorise similarities in the solution space.
Document type :
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Tiphaine Turpin Connect in order to contact the contributor
Submitted on : Tuesday, November 24, 2009 - 9:56:46 AM
Last modification on : Wednesday, February 2, 2022 - 3:51:00 PM
Long-term archiving on: : Monday, October 22, 2012 - 12:40:24 PM


Files produced by the author(s)


  • HAL Id : inria-00433820, version 2


Frédéric Besson, Thomas Jensen, Tiphaine Turpin. Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs. [Research Report] PI 1939, 2009, pp.25. ⟨inria-00433820v2⟩



Record views


Files downloads