Automated reasoning for proving non-orderability of groups

TL;DR

This paper presents a method using automated theorem proving to determine when groups cannot be ordered, leveraging tools like positive cones and torsions to automate the proof process.

Contribution

It introduces a novel automated approach for proving non-orderability of groups, integrating multiple algebraic tools into the theorem proving process.

Findings

Successfully applied automated theorem proving to various groups

Identified criteria for non-orderability using automated methods

Enhanced understanding of group orderability through automation

Abstract

We demonstrate how a generic automated theorem prover can be applied to establish the non-orderability of groups. Our approach incorporates various tools such as positive cones, torsions, generalised torsions and cofinal elements.