Diferencia entre revisiones de «Proyectos relacionados»
(→Propuesta de Proyectos Fin de Grado) |
|||
Línea 3: | Línea 3: | ||
# A. Bundy [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P007 An elementary, machine assisted proof of a multilinear generalisation of the Cauchy-Schwarz inequality]. | # A. Bundy [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P007 An elementary, machine assisted proof of a multilinear generalisation of the Cauchy-Schwarz inequality]. | ||
# A. Bundy [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P012 Heuristic Measures for Controlling Proof Search in a Model Elimination Prover]. | # A. Bundy [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P012 Heuristic Measures for Controlling Proof Search in a Model Elimination Prover]. | ||
+ | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/05-06/Isabelle_Recommender.html Recommender system for an interactive theorem prover]. | ||
# J. Fleuriot [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P032 Mechanical Verification in Isabelle using Powerlists]. | # J. Fleuriot [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P032 Mechanical Verification in Isabelle using Powerlists]. | ||
# J, Fleuriot [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P033 A PRESS Package for Isabelle]. | # J, Fleuriot [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P033 A PRESS Package for Isabelle]. |
Revisión del 08:57 24 oct 2008
En esta sección se recogen enlaces a proyectos de otros grupos que trabajan en los mismos temas que el nuestro.
Propuesta de Proyectos Fin de Grado
- A. Bundy An elementary, machine assisted proof of a multilinear generalisation of the Cauchy-Schwarz inequality.
- A. Bundy Heuristic Measures for Controlling Proof Search in a Model Elimination Prover.
- A. Bundy Recommender system for an interactive theorem prover.
- J. Fleuriot Mechanical Verification in Isabelle using Powerlists.
- J, Fleuriot A PRESS Package for Isabelle.
- J. Fleuriot Experiments in Formalized Mathematics: More Integration Theory in Isabelle/HOL.
- I. Stark Machine formalization of the continuous pi-calculus.