. .

Muscadet 3 Dominique PASTRE Crip5 - Université Paris Descartes pastre(at)math-info(dot)univ-paris5(dot)fr
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.tar.gz
Cette page Web va être redéveloppée.	This Web page is under re-development.
mode d'emploi 3 sept 2008	directions for use 3 sept 2008
manuel-fr.ps est le manuel de l'utilisateur (version 2) Les principales différences de la version 3 sont dans diff-v2-v3-fr	manual-en.ps is the user's manual (version 2) The main differences with version 3 are in diff-v2-v3-en
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 , casc 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
exemples est un répertoire d'exemples (version 2) avec un fichier de définitions donnees, un fichier theoremes et quatre fichiers de traces res_th1, res_th2, res_th3, res_th4.	examples is a directory of examples (version 2) with a file of definitions data, a file theorems and four files of traces resu_th1, resu_th2, resu_th3, resu_th4.
exemples-de-CASC-2005-et-2006 est un autre répertoire d'exemples (version 2).	examples-from-CASC-2005-et-2006 is another directory of examples (version 3).
un exemple de la version 3 et un exemple du 2nd ordre (à compléter)	an example from version 3 and a 2nd order example (to be completed)
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 pl	and which is called by the command pl
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. Utilisation sous Prolog Appeler le script Unix musca-fr . On est alors sous SWI-Prolog et le fichier muscadet-fr est chargé.	1. Use under Prolog Call the Unix script musca-en . You are then under SWI-Prolog and the file muscadet-en is loaded.
1.1. Démonstration directe d'un théorème T demontrer(T). auparavant, si nécessaire, assert(definition(D)). et/ou assert(lemme(Nom,L)). puis consreg.	1.1. Direct proof of a theorem T prove(T). before, if necessary, assert(definition(D)). and/or assert(lemma(Nom,L)). then buildrules.
1.2. Démonstration d'un théorême de la bibliothèque TPTP	1.2. Proof of one theorem of the TPTP library
( http://www.cs.miami.edu/~tptp )
Appeler sous Prolog tptp(Probleme[,Temps]). ou tptp(Domaine,I,J[,Temps]). tptp. décrit la commande tptp et ses options en détail avec des exemples. La preuve detaillée se trouvera dans le fichier res_Probleme suivie des seules étapes utiles. casc(Probleme). donne les seules étapes utiles, sur la sortie standard (voir casc.) pour les details.	Call under Prolog tptp(Problem[,Time]). or tptp(Domain,I,J[,Time]). tptp. describes the command tptp and its options in detail with examples. The detailed proof will be in the file res_Problem followed by the only useful steps. casc(Problem). gives the only useful steps, on the standard output (See casc.) for details.
1.3. Démonstration d'un théorème à partir d'un fichier contenant son énoncé et des données (définitions, lemmes) Appeler sous Prolog th(Fichier). th. indique comment saisir les énoncés. Voir aussi exemple-th	1.3. Proof of a theorem from a file containing its statement and data (definitions, lemmas) Call under Prolog th(File). th. explains how to write the statements. See also example-th
2. Démonstration directe sous Unix d'un théorème avec un exécutable	2. Direct proof under Unix of a theorem from an executable
2.1.Compiler le fichier C tptp-fr.c . Appeler l'exécutable avec comme paramètres un problème TPTP (nom, fichier ou chemin) ou un domaine et deux indices et éventuellement un temps limite. La preuve detaillee suivie des seules étapes utiles se trouvera dans le fichier res_nom-du-problème ou Compiler le fichier C casc-fr.c . Appeler l'exécutable avec comme paramètres un problème TPTP (fichier ou chemin) Les seules étapes utiles de la preuve seront sur la sortie standard.	2.1.Compile the C file tptp-en.c . Run the executable with as parameters a problem TPTP (name, file or path) or a domain and two numbers and eventually a limit time. The detailed proof followed by the only useful steps will be in the file res_problem-name or Compile le fichier C casc-en.c . Run the executable with as parameters a problem TPTP (fichier ou chemin) The only useful steps of the proof will be on the standard output.
2.2.Compiler le fichier C th-fr.c . Appeler l'exécutable avec comme paramètres le nom du fichier où se trouvent l'énoncé du thérème et les données. La preuve détaillée sera sur la sortie standard.	2.2.Compile the C file th-en.c . Run the executable with as parameters the name of the file containing the statement of the theorem to be proved and the data. The detailed proof will be on the standard output.