# 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)

## Abstract

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.

## Keywords

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.

## References

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.
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.
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.
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.
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.
11. 11.
R. Hähnle. Short conjunctive normal forms in finitely-valued logics. Journal of Logic and Computation, 4 (6): 905–927, 1994.
12. 12.
R. Hähnle. Exploiting data dependencies in many-valued logics. Journal of Applied Non-Classical Logics, 6 (1): 49–69, 1996.
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.
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.
21. 21.
D. Mundici. Interpretation of AF C’-algebras in Lukasiewicz sentential calculus. Journal of Functional Analysis, 65: 15–63, 1986.
22. 22.
D. Mundici. Satisfiability in many-valued sentential logic is NP-complete. Theoretical Computer Science, 52: 145–153, 1987.
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.
25. 25.
D. Mundici and G. Panti. Extending addition in Elliott’s local semigroup. Journal of Functional Analysis, 171: 461–472, 1993.
26. 26.
G. Panti. A geometric proof of the completeness of the Lukasiewicz calculus. Journal of Symbolic Logic, 60 (2): 563–578, June 1995.
27. 27.
D. A. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2: 293–304, 1986.
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.
31. 31.
A. Schrijver. Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics. John Wiley and Sons, 1986.
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