The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
From MaRDI portal
Publication:1182164
DOI10.1016/0004-3702(91)90009-9zbMath0736.68071MaRDI QIDQ1182164
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
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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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