Proof Theory of Many-Valued Logic and Linear Optimization

  • Reiner Hähnle
Conference paper
Part of the Advances in Soft Computing book series (AINSC, volume 8)


A simple reduction of two-valued logic to certain linear integer programs is well-known for a long time. This relationship can be extended to any finite-valued and to a large class of infinite-valued logics, for instance to Lukasiewicz and Gödel logics. The resulting reduction is deterministic and has linear cost which makes it feasible to implement satisfiability checking in such logics via linear optimization methods. The reduction is based on semantic tableau methods that are enriched by certain arithmetic constraints. This technique is principally applicable to non-arithmetic constraints as well which opens a general approach to non-classical deduction.


Mixed Integer Programming Classical Logic Proof Theory Linear Polynomial Classical Propositional Logic 
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.
    M. Baaz and C. G. Fermüller. Resolution-based theorem proving for many-valued logics. Journal of Symbolic Computation, 19 (4): 353–391, Apr. 1995.MathSciNetMATHCrossRefGoogle Scholar
  2. 2.
    E. Balas. Disjunctive programming Annals of Discrete Mathematics, 5(Discrete Optimization II):3–51, 1979. Proc. of the Advanced Research Institute on Discrete Optimization and Systems Applications of the Systems Science Panel of NATO and of the Discrete Optimization Symposium, Canada 1977. Edited by P. L. Hammer, E. L. Johnson, and B. H. Korte.Google Scholar
  3. 3.
    C. Bell, A. Nerode, R. Ng, and V. Subrahmanian. Mixed integer programming methods for computing nonmonotonic deductive databases. Journal of the ACM, 41 (6): 1178–1215, Nov. 1994.MathSciNetMATHCrossRefGoogle Scholar
  4. 4.
    W. A. Carnielli. Systematization of finite many-valued logics through the method of tableaux. Journal of Symbolic Logic, 52 (2): 473–493, June 1987.MathSciNetMATHCrossRefGoogle Scholar
  5. 5.
    R. Cignoli and D. Mundici. An invitation to Chang’s MV algebras. In M. Droste and R. Göbel, editors, Advances in algebra and model theory: selected surveys presented at conferences in Essen, 1994 and Dresden, 1995, number 9 in Algebra, logic and applications. Gordon and Breach, Amsterdam, 1997.Google Scholar
  6. 6.
    R. L. O. Cignoli, I. M. L. D’Ottaviano, and D. Mundici. Algebras das Lógicas de Lukasiewicz (in Portuguese), volume 12 of Coleçâo CLE. Centro de Logica, Epistemologiae Historia da Ciênca, Unicamp, Campinas, Brazil, 1995.Google Scholar
  7. 7.
    M. C. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, New York, second edition, 1996.MATHCrossRefGoogle Scholar
  8. 8.
    R. Hähnle. Towards an efficient tableau proof procedure for multiple-valued logics. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, Selected Papers from Computer Science Logic, CSL’90, Heidelberg, Germany, volume 533 of LNCS, pages 248–260. Springer-Verlag, 1991.Google Scholar
  9. 9.
    R. Hähnle. Automated Deduction in Multiple-Valued Logics, volume 10 of International Series of Monographs on Computer Science. Oxford University Press, 1994.Google Scholar
  10. 10.
    R. Hähnle. Many-valued logic and mixed integer programming Annals of Mathematics and Artificial Intelligence, 12 (3,4): 231–264, Dec. 1994.MathSciNetMATHCrossRefGoogle Scholar
  11. 11.
    R. Hähnle. Short conjunctive normal forms in finitely-valued logics. Journal of Logic and Computation, 4 (6): 905–927, 1994.MathSciNetMATHCrossRefGoogle Scholar
  12. 12.
    R. Hähnle. Exploiting data dependencies in many-valued logics. Journal of Applied Non-Classical Logics, 6 (1): 49–69, 1996.MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    R. Hähnle. Proof theory of many-valued logic-linear optimization-logic design: Connections and interactions. Soft Computing-A Fusion of Foundations, Methodologies and Applications, 1 (3): 107–119, Sept. 1997.Google Scholar
  14. 14.
    R. Hähnle and W. Kernig. Verification of switch level designs with many-valued logic. In A. Voronkov, editor, Proc. LPAR’93, St. Petersburg, Russia, volume 698 of LNCS, pages 158–169. Springer-Verlag, 1993.Google Scholar
  15. 15.
    P. V. Hentenryck and T. Graf. Standard Forms for Rational Linear Arithmetics in Constraint Logic Programming. Annals of Mathematics and Artificial Intelligence, 5 (2–4), 1992.Google Scholar
  16. 16.
    J. N. Hooker. A quantitative approach to logical inference. Decision Support Systems, 4: 45–69, 1988.CrossRefGoogle Scholar
  17. 17.
    J. N. Hooker. New methods for computing inferences in first order logic. Annals of Operations Research,43(1–4):479–492, Oct. 1993. Selected Papers of Applied Mathematical Programming and Modelling, APMOD91.Google Scholar
  18. 18.
    J. L. Imbert and P. V. Hentenryck. Efficient Handling of Disequations in CLP over Linear Rational Arithmetics. In F. Benhamou and A. Colmerauer, editors, Constraint Logic Programming: Selected Research, pages 49–71. MIT Press, 1993.Google Scholar
  19. 19.
    R. G. Jeroslow. Logic-Based Decision Support. Mired Integer Model Formulation. Elsevier, Amsterdam, 1988.Google Scholar
  20. 20.
    R. McNaughton. A theorem about infinite-valued sentential logic. Journal of Symbolic Logic, 16 (1): 1–13, 1951.MathSciNetMATHCrossRefGoogle Scholar
  21. 21.
    D. Mundici. Interpretation of AF C’-algebras in Lukasiewicz sentential calculus. Journal of Functional Analysis, 65: 15–63, 1986.MathSciNetMATHGoogle Scholar
  22. 22.
    D. Mundici. Satisfiability in many-valued sentential logic is NP-complete. Theoretical Computer Science, 52: 145–153, 1987.MathSciNetMATHCrossRefGoogle Scholar
  23. 23.
    D. Mundici. Algebras of Ulam’s games with lies. In Proceedings SILFS International Congress, Viareggio, 1990.Google Scholar
  24. 24.
    D. Mundici. A constructive proof of McNaughton’s Theorem in infinite-valued logic. Journal of Symbolic Logic, 59 (2): 596–602, June 1994.MathSciNetMATHCrossRefGoogle Scholar
  25. 25.
    D. Mundici and G. Panti. Extending addition in Elliott’s local semigroup. Journal of Functional Analysis, 171: 461–472, 1993.MathSciNetCrossRefGoogle Scholar
  26. 26.
    G. Panti. A geometric proof of the completeness of the Lukasiewicz calculus. Journal of Symbolic Logic, 60 (2): 563–578, June 1995.MathSciNetMATHCrossRefGoogle Scholar
  27. 27.
    D. A. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2: 293–304, 1986.MathSciNetMATHCrossRefGoogle Scholar
  28. 28.
    G. Rousseau. Sequents in many valued logic I. Fundamenta Mathematics, LX: 23–33, 1967.Google Scholar
  29. 29.
    T. Sasao. Multiple-valued decomposition of generalized Boolean functions and the complexity of programmable logic arrays. IEEE Transactions on Computers, C-30: 635–643, Sept. 1981.Google Scholar
  30. 30.
    B. Scarpellini. Die Nichtaxiomatisierbarkeit des unendlichwertigen Prädikatenkalküls von Lukasiewicz. Journal of Symbolic Logic, 27 (2): 159–170, June 1962.MathSciNetCrossRefGoogle Scholar
  31. 31.
    A. Schrijver. Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics. John Wiley and Sons, 1986.MATHGoogle Scholar
  32. 32.
    J. Siekmann and G. Wrightson, editors. Automation of Reasoning: Classical Papers in Computational Logic 1967–1970, volume 2. Springer-Verlag, 1983.Google Scholar
  33. 33.
    R. M. Smullyan. First-Order Logic. Dover Publications, New York, second corrected edition, 1995. First published 1968 by Springer-Verlag.Google Scholar
  34. 34.
    M. Takahashi. Many-valued logics of extended Gentzen style I. Science Reports of the Tokyo Kyoiku Daigaku, Section A,9(231):95–116, 1967. MR 37.39, Zbl 172.8.Google Scholar
  35. 35.
    G. Tseitin. On the complexity of proofs in propositional logics. Seminars in Mathematics,8, 1970. Reprinted in [32].Google Scholar
  36. 36.
    R. Zach. Proof theory of finite-valued logics. Master’s thesis, Institut für Algebra and Diskrete Mathematik, TU Wien, Sept. 1993. Available as Technical Report TUW-E185.2-Z.1–93.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Reiner Hähnle
    • 1
  1. 1.Institute for Logic, Complexitiy and Deduction Systems Department of Computer ScienceUniversity of KarlsruheKarlsruheGermany

Personalised recommendations