The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning

DOI10.1016/0004-3702(91)90009-9zbMath0736.68071OpenAlexW1970861542MaRDI QIDQ1182164

Alan M. Frisch

Publication date: 28 June 1992

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

Full work available at URL: https://doi.org/10.1016/0004-3702(91)90009-9

zbMATH Keywords

sorted logicssubstitutional framework

Mathematics Subject Classification ID

Related Items (17)

A resolution principle for constrained logics ⋮ Completion for constrained term rewriting systems ⋮ Hybrid reasoning using universal attachment ⋮ Hybridizing nonmonotonic inheritance with theorem proving ⋮ Limited reasoning in first-order knowledge bases with full introspection ⋮ On Skolemization in constrained logics ⋮ Unification in sort theories and its applications ⋮ An order-sorted resolution in theory and practice ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Tableau methods for a logic with term declarations ⋮ Connection calculus theorem proving with multiple built-in theories ⋮ Building Theorem Provers ⋮ A mechanization of strong Kleene logic for partial functions ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ A practical integration of first-order reasoning and decision procedures ⋮ A typed resolution principle for deduction with conditional typing theory ⋮ Order-sorted logic programming with predicate hierarchy

Cites Work

• Towards a general theory of action and time
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• Schubert's steamroller problem: Formulations and solutions
• A more expressive formulation of many sorted logic
• Computational aspects of an order-sorted logic with term declarations
• Automated deduction by theory resolution
• Login: a logic programming language with built-in inheritance
• An Efficient Unification Algorithm
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning