Tableaux for Maximum Satisfiability in Lukasiewicz Logic

Abstract : We define a tableau calculus for solving the MaxSAT problem of 3-valued Lukasiewicz logic, and prove its soundness and completeness. The calculus can be naturally extended to other finitely-valued logics. Our contributions establish the foundations of a generic problem solving paradigm for combinatorial optimization based on Lukasiewicz logic.