On anti-links

  • Bernhard Beckert
  • Reiner Hähnle
  • Anavai Ramesh
  • Neil V. Murray
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 822)


The concept of anti-link is defined, and useful equivalence-preserving operations on propositional formulas based on anti-links are introduced. These operations eliminate a potentially large number of subsumed paths in a negation normal form formula. The operations have linear time complexity in the size of that part of the formula containing the anti-link.

These operations are useful for prime implicant/implicate algorithms because most of the computational effort in such algorithms is spent on subsumption checks.


Conjunctive Normal Form Disjunctive Normal Form Empty Graph Conjunctive Normal Form Formula Prime Implicants 
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.
    de Kleer, J. An improved incremental algorithm for computing prime implicants. Proceedings of AAAI-92, 780–785.Google Scholar
  2. 2.
    Jackson, P., and Pais, J. Computing prime implicants. Proceedings of CADE-10, Kaiserslautern, W. Germany, July, 1990. In LNAI, Springer-Verlag, Vol. 449, 543–557.Google Scholar
  3. 3.
    Jackson, P. Computing prime implicants incrementally. Proceedings of CADE-11, Saratoga Springs, NY, June, 1992. In LNAI, Springer-Verlag, Vol. 607, 253–267.Google Scholar
  4. 4.
    Kean, A., and Tsiknis, G. An incremental method for generating prime implicants/implicates. Journal of Symbolic Computation 9 (1990), 185–206.Google Scholar
  5. 5.
    Kean, A., and Tsiknis, G. Assumption based reasoning and clause management systems. Computational Intelligence 8, 1 (Nov. 1992), 1–24.Google Scholar
  6. 6.
    Letz, R. First-order calculi and proof procedures for automated deduction. Ph.D. thesis, TH Darmstadt, June 1993.Google Scholar
  7. 7.
    Murray, N.V., and Rosenthal, E. Inference with path resolution and semantic graphs. J.ACM 34, 2 (April 1987), 225–254.Google Scholar
  8. 8.
    Murray, N.V., and Rosenthal, E. Path dissolution: A strongly complete rule of inference. Proceedings of AAAI-87, Seattle, WA, July 12–17, 1987, 161–166.Google Scholar
  9. 9.
    Murray, N.V., and Rosenthal, E. Dissolution: Making paths vanish. J.ACM 40, 3 (July 1993), 504–535.Google Scholar
  10. 10.
    Ngair,T. A new algorithm for incremental prime implicate generation. Proceedings of IJCAI-93, Chambery, France, August, 1993.Google Scholar
  11. 11.
    Przymusinski, T.C. An algorithm to compute circumscription. Artificial Intelligence 38 (1989), 49–73.Google Scholar
  12. 12.
    Ramesh, A., and Murray, N.V. Non-clausal deductive techniques for computing prime implicants and prime implicates. Proceedings of LPAR-93. St. Petersburg, Russia, July 13–20, 1993. In LNAI, Springer-Verlag, Vol. 698, 277–288.Google Scholar
  13. 13.
    Reiter, R. and de Kleer, J. Foundations of assumption-based truth maintenance systems: preliminary report. Proceedings of AAAI-87, Seattle, WA, July 12–17, 1987, 183–188.Google Scholar
  14. 14.
    Slagle, J.R., Chang, C.L., and Lee, R.C.T. A new algorithm for generating prime implicants. IEEE Transactions on Computers, C-19(4) (1970), 304–310.Google Scholar
  15. 15.
    Strzemecki, T. Polynomial-time algorithms for generation of prime implicants. Journal of Complexity 8 (1992), 37–63.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Bernhard Beckert
    • 1
  • Reiner Hähnle
    • 1
  • Anavai Ramesh
    • 2
  • Neil V. Murray
    • 2
  1. 1.Institute for Logic, Complexity and Deduction SystemsUniversität KarlsruheKarlsruheGermany
  2. 2.Institute for Programming & Logics, Department of Computer ScienceUniversity at AlbanyAlbany

Personalised recommendations