Proof Theory of Many-Valued Logic and Linear Optimization
Reiner Hähnle · 2001
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.