Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics
Logic in Computer Science
2007-05-23 v1
Abstract
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.
Keywords
Cite
@article{arxiv.cs/0211021,
title = {Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics},
author = {G. Metcalfe and N. Olivetti and D. Gabbay},
journal= {arXiv preprint arXiv:cs/0211021},
year = {2007}
}
Comments
35 pages, 1 figure