A Mechanical Solution of Schubert’s Steamroller by Many-Sorted Resolution

Christoph Walther

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 until now. Our solution clearly demonstrates the power of a many-sorted resolution calculus. The proposed method is applicable to all resolution-based inference systems.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.