Ordering theorems, characterizing when partial orders of a group extend to total orders, are used to generate hypersequent calculi for varieties of lattice-ordered groups (ℓ-groups). These calculi are then used to provide new proofs of theorems arising in the theory of ordered groups. More precisely: an analytic calculus for abelian ℓ-groups is generated using an ordering theorem for abelian groups; a calculus is generated for ℓ-groups and new decidability proofs are obtained for the equational theory of this variety and extending finite subsets of free groups to right orders; and a calculus for representable ℓ-groups is generated and a new proof is obtained that free groups are orderable.
CITATION STYLE
Colacito, A., & Metcalfe, G. (2017). Proof theory and ordered groups. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10388 LNCS, pp. 80–91). Springer Verlag. https://doi.org/10.1007/978-3-662-55386-2_6
Mendeley helps you to discover research relevant for your work.