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 reasoning from the first principles, positive cones, torsions, generalised torsions and cofinal elements.
Paper
References (80)
Scroll for more · 38 remaining