Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics

2002/11/18 by G. Metcalfe, George Metcalfe, Nicola Olivetti +6
Computer Science · #Advanced Algebra and Logic #F.4.1 #FOS: Computer and information sciences #I.2.3 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #cs.LO

paper · pdf · doi:10.48550/arxiv.cs/0211021

35 pages, 1 figure

arxiv created 2002/11/18 · openalex publication_date 2002/11/18 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Superabelian logics
• A note on bases of admissible rules of proper axiomatic extensions of Lukasiewicz logic
• An algebraic study of the first order version of some implicational fragments of the three-valued Lukasiewicz logic
• Strong standard completeness theorems for S5-modal Lukasiewicz logics
• A general view of the algebraic semantics of Łukasiewicz logic with product