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

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