A typed resolution principle for deduction with conditional typing theory

DOI10.1016/0004-3702(94)00027-XzbMath1013.68536OpenAlexW1995495038MaRDI QIDQ1855225

Tie-Cheng Wang

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• ML

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