A mechanical solution of Schubert's steamroller by many-sorted resolution (Q1060859)

We demonstrate the advantage of using a many-sorted resolution calculus by a mechanical solution of a challenge problem. This problem known as 'Schubert's Steamroller' had been unsolved by automated theorem provers before. Our solution clearly demonstrates the power of a many-sorted resolution calculus. The proposed method is applicable to all resolution- based inference systems.