Boolean Approximation Revisited

  • Peter Schachte
  • Harald Søndergaard
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4612)


Most work to date on Boolean approximation assumes that Boolean functions are represented by formulas in conjunctive normal form. That assumption is appropriate for the classical applications of Boolean approximation but potentially limits wider use. We revisit, in a lattice-theoretic setting, so-called envelopes and cores in propositional logic, identifying them with upper and lower closure operators, respectively. This leads to recursive representation-independent characterisations of Boolean approximation for a large class of classes. We show that Boolean development can be applied in a representation-independent setting to develop approximation algorithms for a broad range of Boolean classes, including Horn and Krom functions.


Boolean Function Propositional Logic Closure Operator Conjunctive Normal Form Propositional Knowledge 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Birkhoff, G.: Lattice Theory, 3rd edn. American Mathematical Society (1973)Google Scholar
  2. 2.
    Brace, K., Rudell, R., Bryant, R.: Efficient implementation of a BDD package. In: Proc. Twenty-seventh ACM/IEEE Design Automation Conf., pp. 40–45 (1990)Google Scholar
  3. 3.
    Cadoli, M., Scarcello, F.: Semantical and computational aspects of Horn approximations. Artificial Intelligence 119, 1–17 (2000)zbMATHCrossRefGoogle Scholar
  4. 4.
    Codish, M., Søndergaard, H., Stuckey, P.J.: Sharing and groundness dependencies in logic programs. ACM Transactions on Programming Languages and Systems 21(5), 948–976 (1999)CrossRefGoogle Scholar
  5. 5.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E.J. (ed.) Formal Description of Programming Concepts, pp. 237–277. North-Holland, Amsterdam (1978)Google Scholar
  6. 6.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. Sixth ACM Symp. Principles of Programming Languages, pp. 269–282. ACM Press, New York (1979)Google Scholar
  7. 7.
    Dechter, R., Pearl, J.: Structure identification in relational data. Artificial Intelligence 58, 237–270 (1992)zbMATHCrossRefGoogle Scholar
  8. 8.
    del Val, A.: First order LUB approximations: Characterization and algorithms. Artificial Intelligence 162, 7–48 (2005)CrossRefGoogle Scholar
  9. 9.
    Giacobazzi, R.: Semantic Aspects of Logic Program Analysis. PhD thesis, University of Pisa, Italy (1993)Google Scholar
  10. 10.
    Halmos, P.R.: Lectures on Boolean Algebras. Springer, Heidelberg (1963)zbMATHGoogle Scholar
  11. 11.
    Horiyama, T., Ibaraki, T.: Ordered binary decision diagrams as knowledge-bases. Artificial Intelligence 136, 189–213 (2002)zbMATHCrossRefGoogle Scholar
  12. 12.
    Horiyama, T., Ibaraki, T.: Translation among CNFs, characteristic models and ordered binary decision diagrams. Inf. Processing Letters 85, 191–198 (2003)CrossRefGoogle Scholar
  13. 13.
    Kautz, H., Kearns, M., Selman, B.: Horn approximations of empirical data. Artificial Intelligence 74, 129–145 (1995)zbMATHCrossRefGoogle Scholar
  14. 14.
    Kavvadias, D., Papadimitriou, C., Sideri, M.: On Horn envelopes and hypergraph transversals. In: Ng, K.W., Balasubramanian, N.V., Raghavan, P., Chin, F.Y.L. (eds.) ISAAC 1993. LNCS, vol. 762, pp. 399–405. Springer, Heidelberg (1993)Google Scholar
  15. 15.
    Khardon, R.: Translating between Horn representations and their characteristic models. Journal of Artificial Intelligence Research 3, 349–372 (1995)zbMATHGoogle Scholar
  16. 16.
    Ore, O.: Combinations of closure relations. Ann. Math. 44(3), 514–533 (1943)CrossRefGoogle Scholar
  17. 17.
    Pelletier, F.J., Martin, N.M.: Post’s functional completeness theorem. Notre Dame Journal of Formal Logic 31(2) (1990)Google Scholar
  18. 18.
    Post, E.L.: The Two-Valued Iterative Systems of Mathematical Logic. Princeton University Press, 1941. Reprinted in Davis, M., Solvability, Provability, Definability: The Collected Works of Emil L. Post, pp. 249–374, Birkhaüser (1994)Google Scholar
  19. 19.
    Rudeanu, S.: Boolean Functions and Equations. North-Holland, Amsterdam (1974)zbMATHGoogle Scholar
  20. 20.
    Schachte, P., Søndergaard, H.: Closure operators for ROBDDs. In: Emerson, E.A., Namjoshi, K. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 1–16. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  21. 21.
    Schaefer, T.J.: The complexity of satisfiability problems. In: Proc. Tenth Ann. ACM Symp. Theory of Computing, pp. 216–226 (1978)Google Scholar
  22. 22.
    Selman, B., Kautz, H.: Knowledge compilation and theory approximation. Journal of the ACM 43(2), 193–224 (1996)zbMATHCrossRefGoogle Scholar
  23. 23.
    Ward, M.: The closure operators of a lattice. Ann. Math. 43(2), 191–196 (1942)CrossRefGoogle Scholar
  24. 24.
    Zanuttini, B.: Approximating propositional knowledge with affine formulas. In: ECAI 2002. Proceedings of the Fifteenth European Conference on Artificial Intelligence, pp. 287–291. IOS Press, Amsterdam (2002)Google Scholar
  25. 25.
    Zanuttini, B.: Approximation of relations by propositional formulas: Complexity and semantics. In: Koenig, S., Holte, R.C. (eds.) SARA 2002. LNCS (LNAI), vol. 2371, pp. 242–255. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Peter Schachte
    • 1
  • Harald Søndergaard
    • 1
  1. 1.NICTA Victoria Laboratory, Department of Computer Science and Software Engineering, The University of Melbourne, Vic. 3010Australia

Personalised recommendations