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.
Type de document :
Rapport
[Research Report] PI 1939, 2009, pp.25
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00433820
Contributeur : Tiphaine Turpin <>
Soumis le : mardi 24 novembre 2009 - 09:56:46
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : lundi 22 octobre 2012 - 12:40:24

Fichier

PI-1939.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

458

Téléchargements de fichiers

147