Finite satisfiability in infinite-valued Lukasiewicz logic

Although it is well-known that every satisfiable formula in Łukasiewicz’ infinite-valued logic L∞ can be satisfied in some finite-valued logic, practical methods for finding an appropriate number of truth degrees do currently not exist. As a first step towards efficient reasoning in L∞ , we propose a method to find a tight upper bound on this number which, in practice, often significantly improves the worst-case upper bound of Aguzzoli et al