A mechanical solution of Schubert's steamroller by many-sorted resolution (Q1060859): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/0004-3702(85)90029-3 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2107046473 / rank | |||
Normal rank | |||
Revision as of 21:52, 19 March 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A mechanical solution of Schubert's steamroller by many-sorted resolution |
scientific article |
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
