Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics

Metcalfe, G.; Olivetti, N.; Gabbay, D.

Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics

Authors

Metcalfe, G.

Olivetti, N.

Gabbay, D.

Description

We present two embeddings of infinite-valued 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 for A and L and terminating versions of these calculi; labelled single sequent calculi for A and L of complexity co-NP; unlabelled single sequent calculi for A and L.
35 pages, 1 figure