Boolean functions for dependency analysis: algebraic properties and efficient representation

Tania Armstrong, Kim Marriott, Peter Schachte, Harald Søndergaard

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

38 Citations (Scopus)


Many analyses for logic programming languages use Boolean functions to express dependencies between variables or argument positions. Examples include groundness analysis, arguably the most important analysis for logic programs, finiteness analysis and functional dependency analysis. We identify two classes of Boolean functions that have been used: positive and definite functions, and we systematically investigate these classes and their efficient implementation for dependency analyses. We provide syntactic characterizations and study their algebraic properties. In particular, we show that both classes are closed under existential quantification. We investigate representations for these classes based on: reduced ordered binary decision diagrams (ROBDDs), disjunctive normal form, conjunctive normal form, Blake canonical form, dual Blake canonical form, and a form specific to definite functions. We give an empirical comparison of these different representations for groundness analysis.

Original languageEnglish
Title of host publicationStatic Analysis - 1st International Static Analysis Symposium, SAS '94, Proceedings
EditorsBaudouin Le Charlier
Number of pages15
ISBN (Print)9783540584858
Publication statusPublished - 1994
EventStatic Analysis Symposium 1994 - Namur, Belgium
Duration: 28 Sep 199430 Sep 1994
Conference number: 1st (Proceedings)

Publication series

NameLecture Notes in Computer Science
Volume864 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceStatic Analysis Symposium 1994
Abbreviated titleSAS 1994
Internet address

Cite this