Title: Complementarity of a Natural Deduction Knowledge-Based Prover and Resolution-Based Provers in Automated Theorem Proving
Abstract: Muscadet is a knowledge-based theorem prover based on natural deduction. The results obtained during the CASC competitions of theorem provers show its complementarity with regard to resolution-based provers. This paper presents some Muscadet proofs of theorems proposed at the last two competitions (2005 and 2006) and points out some of the characteristics which may account for its successes.
Publication Year: 2007
Publication Date: 2007-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 3
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot