A mechanical solution of Schubert's steamroller by many-sorted resolution

DOI10.1016/0004-3702(85)90029-3zbMath0569.68076OpenAlexW2107046473WikidataQ56092433 ScholiaQ56092433MaRDI QIDQ1060859

Christoph Walther

Publication date: 1985

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(85)90029-3

zbMATH Keywords

challenge problem

Mathematics Subject Classification ID

Related Items (22)

Translation of first order formulas into ground formulas via a completion theory ⋮ Resolution for label-based formulas in hierarchical representation ⋮ Reduction and unification in lambda calculi with a general notion of subtype ⋮ CoLab: A hybrid knowledge representation and compilation laboratory ⋮ Seventy-five problems for testing automatic theorem provers ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ A new reduction rule for the connection graph proof procedure ⋮ An order-sorted resolution in theory and practice ⋮ Kernel functions for case-based planning ⋮ An Oxford survey of order sorted algebra ⋮ The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning ⋮ A semantic backward chaining proof system ⋮ An order-sorted logic for knowledge representation systems ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Completing sort hierarchies ⋮ Order-sorted unification ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Deductive synthesis of sorting programs ⋮ A typed resolution principle for deduction with conditional typing theory ⋮ A mechanical solution of Schubert's steamroller by many-sorted resolution ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Order-sorted logic programming with predicate hierarchy

Cites Work

• Investigations in many-sorted quantor logic
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• Problem corner: Reasoning about equality
• Automated deduction by theory resolution
• Die Zulässigkeit der Behandlung mehrsortiger Theorien mittels der üblichen einsortigen Prädikatenlogik
• A theory of restricted quantification I
• Theorem Proving by Covering Expressions
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Logic of many-sorted theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A mechanical solution of Schubert's steamroller by many-sorted resolution