Automated Deduction and Integer Programming

  • Reiner Hähnle
Conference paper
Part of the Collegium Logicum book series (COLLLOGICUM, volume 1)


We generalize propositional semantic tableaux for classical and many-valued logics to constraint tableaux. We show that this technique is a generalization of the standard translation from CNF formulas into integer programming. The main advantages are (i) a relatively efficient satisfiability checking procedure for classical, finitely-valued and, for the first time, for a wide range of infinitely-valued propositional logics; (ii) easy NP-containment proofs for many-valued logics. The standard translation of two-valued CNF formulas into integer programs and Tseitin’s structure preserving clause form translation are obtained as a special case of our approach.


Mixed Integer Programming Conjunctive Normal Form Integer Programming Problem Proof Tree Automate Deduction 
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.
    Mervin G. Beavers. Automated theorem proving for Lukasiewicz logics. Manuscript of talk given at 1991 Meeting of Society for Exact Philosophy, Victoria, Canada, May 1991.Google Scholar
  2. 2.
    Thierry Boy de la Tour. Minimizing the number of clauses by renaming. In Mark E. Stickel, editor, Proc. 10th International Conference on Automated Deduction, Kaiserslautern, pages 558–572. Springer, LNCS 449, July 1990.Google Scholar
  3. 3.
    George B. Dantzig. Linear Programming and Extensions. Princeton University Press, 1963.Google Scholar
  4. 4.
    Reiner Hähnle. Towards an efficient tableau proof procedure for multiple-valued logics. In Proceedings Workshop on Computer Science Logic, Heidelberg, pages 248–260. Springer, LNCS 533, 1990.Google Scholar
  5. 5.
    Reiner Hähnle. Uniform notation of tableaux rules for multiple-valued logics. In Proc. International Symposium on Multiple-Valued Logic, Victoria, pages 238–245. IEEE Press, 1991.Google Scholar
  6. 6.
    Reiner Hähnle. A new translation from deduction into integer programming. In Jacques Calmet and John A. Campbell, editors, Proc. Int. Conf. on Artificial Intelligence and Symbolic Mathematical Computing AISMC-1, Karlsruhe, Germany, pages 262–275. Springer, LNCS 737, 1992.Google Scholar
  7. 7.
    Reiner Hähnle. Automated Deduction in Multiple-Valued Logics, volume 10 of International Series of Monographs on Computer Science. Oxford University Press, 1993.Google Scholar
  8. 8.
    Reiner Hähnle. Short normal forms for arbitrary finitely-valued logics. In Proceedings ISMIS’93, Trondheim, Norway, pages 49–58. Springer LNCS 689, 1993.Google Scholar
  9. 9.
    Reiner Hähnle and Ortrun Ibens. Improving temporal logic tableaux using integer constraints. In Proc. International Conference on Temporal Logic, Bonn, Germany. Springer LNCS, 1994.Google Scholar
  10. 10.
    Reiner Hähnle and Werner Kernig. Verification of switch level designs with many-valued logic. In Andrei Voronkov, editor, Proc. LPAR’93, St. Petersburg, pages 158–169. Springer, LNAI 698, 1993.Google Scholar
  11. 11.
    John N. Hooker. A quantitative approach to logical inference. Decision Support Systems, 4: 45–69, 1988.CrossRefGoogle Scholar
  12. 12.
    John N. Hooker. Logical inference and polyhedral projection. In Proc. Computer Science Logic Workshop 1991, Berne, pages 184–200. Springer, LNCS 626, 1991.Google Scholar
  13. 13.
    Robert G. Jeroslow. Logic-Based Decision Support. Mixed Integer Model Formulation. Elsevier, Amsterdam, 1988.Google Scholar
  14. 14.
    Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1: 167–187, 1990.MATHCrossRefGoogle Scholar
  15. 15.
    Richard M. Karp. Reducibility among combinatorial problems. In R.E. Miller and J.W. Thatcher, editors, Complexity of Computer Computations, pages 85–103. Plenum Press, 1972.Google Scholar
  16. 16.
    Shie-Jue Lee and David A. Plaisted. Eliminating duplication with the hyperlinking strategy. Journal of Automated Reasoning, 9 (l): 25–42, 1992.MathSciNetMATHCrossRefGoogle Scholar
  17. 17.
    Robert McNaughton. A theorem about infinite-valued sentential logic. Journal of Symbolic Logic, 16 (1): 1–13, 1951.MathSciNetMATHCrossRefGoogle Scholar
  18. 18.
    Daniele Mundici. Satisfiability in many-valued sentential logic is NP-complete. Theoretical Computer Science, 52: 145–153, 1987.MathSciNetMATHCrossRefGoogle Scholar
  19. 19.
    Daniele Mundici. The complexity of adaptive error-correcting codes. In Proceedings Workshop Computer Science Logic 90, Heidelberg, pages 300–307. Springer, LNCS 533, 1990.Google Scholar
  20. 20.
    Daniele Mundici. A constructive proof of McNaughton’s Theorem in infinite-valued logic. Journal of Symbolic Logic, to appear, 1994.Google Scholar
  21. 21.
    Daniele Mundici and Massimo Pasquetto. A proof of the completeness of the infinite-valued calculus of Lukasiewicz with one variable. In E..P. Klement and U. Hoehle, editors, Proc. International Conference on Nonclassical Logics and their Applications 1992 in Linz/Austria. Kluwer, 1994.Google Scholar
  22. 22.
    George L. Nemhauser and Laurence A. Wolsey. Integer programing. In G. L. Nemhauser, A. H. G. Rinnooy Kan, and M.J. Todd, editors, Handbooks in Operations Research and Management Science, Vol. II: Optimization, chapter VI, pages 447–527. North-Holland, Amsterdam, 1989.Google Scholar
  23. 23.
    David A. Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2: 293–304, 1986.MathSciNetMATHCrossRefGoogle Scholar
  24. 24.
    David A. Plaisted and Shie-Jue Lee. Inference by clause matching. In Zbigniew Ras and Maria Zemankova, editors, Intelligent Systems—State of the art and future directions, chapter 8, pages 200–235. Ellis Horwood, 1990.Google Scholar
  25. 25.
    Klaus Ries and Reiner Hähnle. Prädikatenlogisches Beweisen mit gemischt ganzzahliger Optimierung. Ein tableaubasierter Ansatz. In Working Notes of Workshop Künstliche Intelligenz und Operations Research, Berlin (published as Tech Report, Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-93-234), 1993.Google Scholar
  26. 26.
    Harvey Salkin and Kamlesh Mathur. Foundations of Integer Programming. North-Holland, 1989.Google Scholar
  27. 27.
    Jörg Siekmann and Graham Wrightson, editors. Automation of Reasoning: Classical Papers in Computational Logic 1967–1970, volume 2. Springer-Verlag, 1983.Google Scholar
  28. 28.
    Raymond Smullyan. First-Order Logic. Springer, New York, 1968.MATHGoogle Scholar
  29. 29.
    G. Tseitin. On the complexity of proofs in propositional logics. Seminars in Mathematics, 8, 1970. Reprinted in [27].Google Scholar
  30. 30.
    Ryszard Wójcicki. Theory of Logical Calculi. Reidel, Dordrecht, 1988.Google Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Reiner Hähnle
    • 1
  1. 1.Institut für Logik, Komplexität und Deduktionssysteme Fakultät für InformatikUniversität KarlsruheKarlsruheGermany

Personalised recommendations