---
title: "On the Solution of Schubert's Steamroller in Many-Sorted Logic"
authors:
  - "Anthony G. Cohn"
doi: ""
url: "https://ijcai.org/proceedings/1985/237"
pdf: "https://ijcai.org/proceedings/1985/0237.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "1169-1173"
track: "Theorem Proving"
keywords:
---

# On the Solution of Schubert's Steamroller in Many-Sorted Logic

Anthony G. Cohn

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 1169-1173.

## Abstract

A challenge problern for automated theorem provers posed in 1978 by Schubert has recently been solved with the Karlsruhe MKRP-system by formulating the problern in many sorted logic. It is shown here that a further improvement is possible by using a more sophisticated, polymorphic many sorted logic . The problern and its solution are discussed and the differences between the different formulations are analysed .