. .
Muscadet 4.2
Dominique PASTRE
LIPADE - 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.tgz


mode d'emploi

april 2011


directions for use

april 2011

manuel-fr.pdf est le manuel de l'utilisateur (version 4.1)

manual-en.pdf is the user's manual (version 4.1)
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
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 appeler
th(Fichier [,Options]).
ou th. pour un mode d'emploi détaillé
2.1. Under Prolog 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]
ou 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
res_
<name of the theorem or of the TPTP problem TPTP>