Strong and weak points of the MUSCADET theorem prover – examples from CASC‐JC

Issue title: CASC

Article type: Research Article

Authors: Pastre, Dominique

Affiliations: Crip5, Université René Descartes – Paris 5, 45 rue des Saints Pères, F‐75270 Paris Cedex, France E‐mail: pastre@math‐info.univ‐paris5.fr

Abstract: MUSCADET is a knowledge‐based theorem prover based on natural deduction. It has participated in CADE Automated theorem proving System Competitions. The results show its complementarity with regard to resolution‐based provers. This paper presents some of its crucial methods and gives some examples of MUSCADET proofs from the last competition (CASC‐JC in IJCAR 2001).

Keywords: Theorem proving, knowledge bases, natural deduction

Journal: AI Communications, vol. 15, no. 2-3, pp. 147-160, 2002