A mechanical solution of Schubert's steamroller by many-sorted resolution (Q1060859)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A mechanical solution of Schubert's steamroller by many-sorted resolution |
scientific article; zbMATH DE number 3909779
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A mechanical solution of Schubert's steamroller by many-sorted resolution |
scientific article; zbMATH DE number 3909779 |
Statements
A mechanical solution of Schubert's steamroller by many-sorted resolution (English)
0 references
1985
0 references
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.
0 references
challenge problem
0 references
0 references
