Complementarity of a Natural Deduction Knowledge-Based Prover and Resolution-Based Provers in Automated Theorem Proving
Dominique Pastre · 2007
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. Key words: automated theorem proving, natural deduction, knowledge-based system 1