A mechanical solution of Schubert's steamroller by many-sorted resolution
type: Item
instance of: scholarly article
title: A mechanical solution of Schubert's steamroller by many-sorted resolution
zbMATH Open document ID: 0569.68076
DOI: 10.1016/0004-3702(85)90029-3
author: Christoph Walther
published in: Artificial Intelligence
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 3909779
zbMATH Keywords: challenge problem
Wikidata QID: Q56092433
MaRDI profile type: Publication
full work available at URL: 0004-3702(85)90029-3
OpenAlex ID: W2107046473
cites work: Q3894958
cites work: Q4184362
cites work: Q5528633
cites work: A theory of restricted quantification I
cites work: Q5685660
cites work: Theorem Proving by Covering Expressions
cites work: Problem corner: Reasoning about equality
cites work: Investigations in many-sorted quantor logic
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Die Zulässigkeit der Behandlung mehrsortiger Theorien mittels der üblichen einsortigen Prädikatenlogik
cites work: Automated deduction by theory resolution
cites work: Q3682461
cites work: Q3992821
cites work: Logic of many-sorted theories
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
description: scientific article; zbMATH DE number 3909779