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

DOI10.1016/0004-3702(91)90009-9zbMath0736.68071MaRDI 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 logics; substitutional framework

Mathematics Subject Classification ID

68T27: Logic in artificial intelligence

Related Items

Building Theorem Provers, Tableau methods for a logic with term declarations, Connection calculus theorem proving with multiple built-in theories, Order-sorted logic programming with predicate hierarchy, A resolution principle for constrained logics, Hybrid reasoning using universal attachment, Hybridizing nonmonotonic inheritance with theorem proving, On Skolemization in constrained logics, Unification in sort theories and its applications, An order-sorted resolution in theory and practice, A typed resolution principle for deduction with conditional typing theory

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