Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/inria-00433820
Contributor : Tiphaine Turpin <>
Submitted on : Tuesday, November 24, 2009 - 9:56:46 AM
Last modification on : Thursday, January 7, 2021 - 4:13:10 PM
Long-term archiving on: : Monday, October 22, 2012 - 12:40:24 PM

File

PI-1939.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00433820, version 2

Citation

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⟩

Share

Metrics

Record views

517

Files downloads

224