A typed resolution principle for deduction with conditional typing theory
From MaRDI portal
Publication:1855225
DOI10.1016/0004-3702(94)00027-XzbMath1013.68536OpenAlexW1995495038MaRDI QIDQ1855225
Publication date: 4 February 2003
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0004-3702(94)00027-x
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Eliminating dublication with the hyper-linking strategy
- A mechanical solution of Schubert's steamroller by many-sorted resolution
- Hierarchical deduction
- A more expressive formulation of many sorted logic
- Non-Horn clause logic programming without contrapositives
- Using sophisticated models in resolution theorem proving
- The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
- A semantic backward chaining proof system
- Non-resolution theorem proving
- A theory of type polymorphism in programming
- A resolution principle for a logic with restricted quantifiers
- Computational aspects of an order-sorted logic with term declarations
- Automated deduction by theory resolution
- Linear resolution with selection function
- On Matrices with Connections
- The Semantics of Predicate Logic as a Programming Language
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- Mechanical Theorem-Proving by Model Elimination
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
This page was built for publication: A typed resolution principle for deduction with conditional typing theory
