Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics

摘要

We present two embeddings of Lukasiewicz logic L into Meyer and Slaney's Abelian logic A, the logic of lattice-ordered Abelian groups. We give new analytic proof systems for A and use the embeddings to derive corresponding systems for L. These include hypersequent calculi, terminating hypersequent calculi, co-NP labeled sequent calculi, and unlabeled sequent calculi.