. .

Muscadet 4 Dominique PASTRE pastre(at)normalesup(dot)org(dot)org
Muscadet est distribué sous	Muscadet is available under
the new BSD licence
Tous les fichiers se trouvent dans l'archive	All files are in the archive
muscadet.tgz
Le démonstrateur de théorèmes Muscadet est un système à base de connaissances. Il est basé sur la déduction naturelle, et utilise des méthodes proches de celles de l'être humain. Il comprend un moteur d'inférences qui interprète et exécute des règles et une ou plusieurs bases de faits qui sont les représentations internes de «théorèmes à démontrer» Les règles sont soit universelles et incorporées au système, soit construites par le système lui-même grâce à des métarègles, à partir des données (définitions et lemmes) fournies par l'utilisateur.	The Muscadet theorem prover is a knowledge-based system. It is based on natural deduction, and uses methods which resemble those used by humans. It is composed of an inference engine, which interprets and executes rules, and of one or several bases of facts, which are the internal representations of "theorems to be proved". Rules are either universal and put into the system, or built by the system itself by metarules from data (definitions and lemmas) given by the user.
mode d'emploi (aussi dans Lisezmoi)	directions for use (also in ReadMe)
manuel-fr.pdf est le manuel de l'utilisateur	manual-en.pdf is the user's manual
muscadet-fr est le fichier Prolog complet	muscadet-en is the complete Prolog file
musca-fr est un script Unix qui permet de lancer le programme. Il faut ensuite utiliser une des commandes demontrer, tptp ou th	musca-en is a Unix script, which allows to start it; you must then call one of the commands prove, tptp , casc or th
th-fr.c et tptp-fr.c sont des petits fichiers C qui permettent de travailler sous Linux	th-en.c and tptp-en.c are small C files which allow to work under Linux
exemples est un répertoire d'exemples (données exemple* et preuves res_*)	examples is a directory of examples (data example* and proofs res_*)
Le Prolog utilisé est SWI-Prolog, logiciel gratuit sous licence L-GPL, téléchargeable à l'adresse suivante	The Prolog used is SWI-Prolog, which is freeware under an L-GPL license, downloaded at the following address
http://www.swi-prolog.org/Download.html
et que l'on appelle par la commande	and which is called by the command
/usr/bin/swipl
Dans tous les cas, se placer dans un répertoire contenant le fichier Prolog muscadet-fr (ou un lien de même nom vers ce fichier). Puis	In all cases, you have to be in a directory that contains the Prolog file muscadet-en (or a link with the same name to this file). Then
1. Démonstration directe d'un théorème T (sous Prolog) Appeler le script Unix musca-fr . On est alors sous SWI-Prolog et le fichier muscadet-fr est chargé.	1. Direct proof of a theorem T (under Prolog) Call the Unix script musca-en . You are then under SWI-Prolog and the file muscadet-en is loaded.
taper demontrer(T). auparavant, si nécessaire, assert(definition(D)). et/ou assert(lemme(Nom,L)). puis consreg.	type prove(T). before, if necessary, assert(definition(D)). and/or assert(lemma(Nom,L)). then buildrules.
2. Démonstrations à partir de fichiers contenant théorèmes, définitions et, lemmes sous la forme theoreme(Nom,T). definition(D). lemme(Nom,L).	2. Proofs from files containing theorems, definitions and lemmas in the form theorem(Nom,T). definition(D). lemma(Name,L).
2.1. Sous Prolog (appelé par musca-fr qui a chargé muscadet-fr), appeler th(Fichier [,Options]). ou th. pour un mode d'emploi détaillé	2.1. Under Prolog (called by musca-en which loads muscadet-en), call th(File [,Options]). or th. for detailed instructions
2.2. Sous Linux compiler le fichier th-fr.c, executable th appeler th fichier [options] ou th pour un mode d'emploi détaillé	2.2. Under Linux compile the file th-en.c, executable th call th file [options] ou th for detailed instructions
3. Démonstration d'un théorême de la bibliothèque TPTP	3. Proof of one theorem of the TPTP library
( http://www.cs.miami.edu/~tptp )
3.1. Sous Prolog (appelé par musca-fr qui a chargé muscadet-fr), appeler tptp(Fichier [,Options]). ou tptp(Nom [,Options]). ou tptp. pour un mode d'emploi détaillé	3.1. Under Prolog (called by musca-en which loads muscadet-en), call tptp(File [,Options]). or tptp(Name[,Options]). or tptp. for detailed instructions
3.2. Sous Linux compiler le fichier tptp-fr.c, executable tptp appeler tptp chemin [options] ou tptp pour un mode d'emploi détaillé	3.2. Under Linux compile the file tptp-en.c, executable tptp call tptp path [options] or tptp for detailed instructions
4. Résultats dans le cas direct (1.), sur la sortie standard sinon (2. et 3.) dans des fichiers appelés res_<nom du théorème ou du problème TPTP>	4. Results in the direct case (1.), on the standard output otherwise (2. et 3.) in files named rul_<name of the theorem or of the TPTP problem TPTP>