Algorithmic problems in Lukasiewicz logic

Abstrakt

This is an expository talk about a range of algorithmic problems in propositional Lukasiewicz logic. Some of them, such as derivability from finite theories or rule admissibility, become particularly prominent in a non-classical setting. The computational study of a logic usually goes from obtaining decidability results to complexity upper bounds to algorithms and implementations. I will provide a brief introduction to Lukasiewicz logic and the class of MV-algebras that forms its equivalent algebraic semantics. Then I will highlight the semantic methods that led to the algorithmic results and discuss some computational milestones, as well as problems that are peculiar to the logic.