Accueil
Plan du site
Bloc notes
Jeux
Graphes
Combinatoire
Arithmétique
Algèbre
Analyse
Probabilités
Automates
Programmation
Divers
Liens
Home
Plan du site
Bloc notes
Jeux
Graphes
Combinatoire
Arithmétique
Algèbre
Analyse
Probabilités
Automates
Programmation
Divers
Liens
Home
UniversitySurf.net
Votre portail e-Learning
Votre portail e-Learning
Séminaire MaMuX
Mathématiques, musique et relations avec d'autres disciplines
Mathématiques, musique et relations avec d'autres disciplines
ZOHO® permet de lire les documents doc ppt pdf...
Cliquez ici
Déduction automatique - AutomatedDeduction
| SOMMAIRE | Groupes | Pages Web | Associations | Projets | Exercices | Exemples |
| Systèmes | Ftp | Données | Journaux | Collections | Liens |
| Systèmes | Ftp | Données | Journaux | Collections | Liens |
GROUPES - GROUPS
at Argonne
<http://www.mcs.anl.gov/AR/>
at The University of Texas at Austin
<http://www.ma.utexas.edu/users/bshults/ATP/>
Edinburgh Dept of AI
<http://dream.dai.ed.ac.uk/>
<http://jswww.cs.uni-sb.de/pub/www/deduktion/research-groups-germany.html>
Institute for New Generation Computer Technolog
<http://www.icot.or.jp/>
at The University of Iowa
<http://www.cs.uiowa.edu/ar/arui.html>
<http://www.mrg.dist.unige.it/>
<http://afrodite.itc.it:1024>
PAGES WEB
by Nachum Dershowitz and Laurent Vigneron.
<http://www.loria.fr/~vigneron/RewritingHP/>
ASSOCIATIONS
<http://mizar.org/>
PROJETS - PROJECTS
<http://www-unix.mcs.anl.gov/qed/>
EXERCICES - EXERCISES
<http://www.cs.cmu.edu:8001/afs/cs/user/fp/www/lfs.html>
EXEMPLES - EXAMPLES
<http://www.informatik.tu-muenchen.de/~tptp>
SYSTÈMES
from the University of Texas
<http://www.cli.com/software/acl2/>
from Cornell
<http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html>
(a Generic Theorem Prover), from Cambridge University
<http://www.cl.cam.ac.uk/users/lcp/ml-aftp/>
(Boyer-Moore Theorem Prover), from the University of Texas
<http://www.cli.com/software/nqthm/index.html>
from Warsaw University
<http://web.cs.ualberta.ca/~piotr/Mizar/>
<http://pauillac.inria.fr/coq>
<http://www.trireme.demon.co.uk/index.html>
(Prototype Verification System), from SRI International
<http://www.csl.sri.com/sri-csl-pvs.html>
Carnegie Mellon University
<http://www.cs.cmu.edu/afs/cs.cmu.edu/user/andrews/www/tps.html>
Proof Assistant
<http://www.dcs.ed.ac.uk/home/lego/>
an Interactive Mathematical Proof System
<file://math.harvard.edu/imps/imps_html/imps.html>
a tableau-based theorem prover
<http://emmy.ira.uka.de/~posegga/leantap/leantap.html>
<http://www.cs.chalmers.se/~tammet/gandalf/>
from Duke University
<http://www.cs.duke.edu/~ola/meteor.html>
from the University of North Carolina
<http://www.cs.unc.edu/~zhu/prover.html>
<http://www.mcs.anl.gov/AR/otter/index.html>
Rewrite Rule Laboratory
<file://cs.uiowa.edu/pub/hzhang/>
<http://wwwjessen.informatik.tu-muenchen.de/~setheo>
<http://wwwjessen.informatik.tu-muenchen.de/~suttner/sptheo.html>
from MPI Saarbrücken
<http://spass.mpi-sb.mpg.de/>
from Kaiserslautern
<http://www.uni-kl.de/AG-AvenhausMadlener/waldmeister.html>
from Wichita State University
<http://www.cs.twsu.edu/~chou/ge.html>
Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine.
<http://coq.inria.fr/>
SITES FTP
<ftp://ftp.mcs.anl.gov/pub/qed/>
DONNÉES - DATAS
<http://www-formal.stanford.edu/clt/ARS/ars-db.html>
JOURNAUX - LETTERS
Journal of Formalized Mathematics is an electronic counterpart of Formalized Mathematics. However it is not the same journal.
<http://mizar.org/JFM/>
COLLECTIONS
<http://www.comlab.ox.ac.uk/archive/formal-methods.html>
LIENS - LINKS
<http://www-unix.mcs.anl.gov/AR/others.html>Actualités
| SOMMAIRE | Groupes | Pages Web | Associations | Projets | Exercices | Exemples |
| Systèmes | Ftp | Données | Journaux | Collections | Liens |
| Systèmes | Ftp | Données | Journaux | Collections | Liens |
Advertising :
If you see a reference in one of the files that is not linked, and you know of a link address to the appropriate document,
please send me mail, and I will include the link in the document. Thanks very much in advance.
Avertissement : Le classement par catégories est approximatif. Certains liens se retrouvent dans des rubriques différentes et sur plusieurs pages. Les commentaires sont généralement des courts extraits des pages référencées. Il est possible que certains liens nécessitent une mise à jour.
Tous commentaires ou remarques sont les bienvenus, vous pouvez les adresser à :
Les mises à jour demandées sont réalisées dès que possible et, sauf si c'est nécessaire, aucun message de réponse n'est expédié. Merci de m'écrire.
Copyright © 1999-2006 Jean-Paul Davalan - Reproduction interdite.
Avertissement : Le classement par catégories est approximatif. Certains liens se retrouvent dans des rubriques différentes et sur plusieurs pages. Les commentaires sont généralement des courts extraits des pages référencées. Il est possible que certains liens nécessitent une mise à jour.
Tous commentaires ou remarques sont les bienvenus, vous pouvez les adresser à :
Les mises à jour demandées sont réalisées dès que possible et, sauf si c'est nécessaire, aucun message de réponse n'est expédié. Merci de m'écrire.
Copyright © 1999-2006 Jean-Paul Davalan - Reproduction interdite.
| Accueil | Plan du site | Bloc notes | Jeux | Graphes | Combinatoire | Arithmétique | Algèbre |
| Analyse | Probabilités | Automates | Informatique | Divers | Lycée |
| Analyse | Probabilités | Automates | Informatique | Divers | Lycée |
