Sequent and hypersequent calculi for abelian and łukasiewicz logics
George Metcalfe, Nicola Olivetti, Dov M. Gabbay · ACM Transactions on Computational Logic · 2005
We present two embeddings of Łukasiewicz logicŁinto Meyer and Slaney's Abelian logicA, the logic of lattice-ordered Abelian groups. We give new analytic proof systems forAand use the embeddings to derive corresponding systems forŁ. These include hypersequent calculi, terminating hypersequent calculi, co-NP labeled sequent calculi, and unlabeled sequent calculi.