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