Diferencia entre revisiones de «Proyectos relacionados»
(→Propuesta de Proyectos de Tesis Doctoral) |
|||
| Línea 1: | Línea 1: | ||
En esta sección se recogen enlaces a proyectos de otros grupos que trabajan en los mismos temas que el nuestro. | En esta sección se recogen enlaces a proyectos de otros grupos que trabajan en los mismos temas que el nuestro. | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | == | + | == Proyectos de investigación == |
| − | # | + | # [http://dream.inf.ed.ac.uk/projects/ontology_evolution/index.html Ontology Evolution in Physics]. |
| − | == | + | == Propuestas de Proyectos de Tesis Doctoral == |
# A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/calculemus.html A Proof Management Tool]. | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/calculemus.html A Proof Management Tool]. | ||
# A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/cynthia-prolog.html A Programming by Analogy Editor for Godel]. | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/cynthia-prolog.html A Programming by Analogy Editor for Godel]. | ||
| Línea 19: | Línea 11: | ||
# A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/phd-project-hardware.html Automatic Hardware Verification]. | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/phd-project-hardware.html Automatic Hardware Verification]. | ||
# A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/rep-evolution.html Ontology Evolution]. | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/rep-evolution.html Ontology Evolution]. | ||
| + | |||
| + | == Propuestas de Proyectos Fin de Master == | ||
| + | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/04-05/zariski.html Proving Zariski Space Theorems in Isabelle: A Case Study in the Application of Automated Theorem Proving to Mathematical Research]. | ||
| + | |||
| + | == Propuestas de Proyectos Fin de Grado == | ||
| + | # 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/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=P033 A PRESS Package for Isabelle]. | ||
| + | # J. Fleuriot [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P034 Experiments in Formalized Mathematics: More Integration Theory in Isabelle/HOL]. | ||
| + | # I. Stark [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P162 Machine formalization of the continuous pi-calculus]. | ||
Revisión del 09:14 24 oct 2008
En esta sección se recogen enlaces a proyectos de otros grupos que trabajan en los mismos temas que el nuestro.
Sumario
Proyectos de investigación
Propuestas de Proyectos de Tesis Doctoral
- A. Bundy A Proof Management Tool.
- A. Bundy A Programming by Analogy Editor for Godel.
- A. Bundy A Teaching Aid for Nonstandard Analysis.
- A. Bundy Synthesis of Decision Procedures.
- A. Bundy Automatic Hardware Verification.
- A. Bundy Ontology Evolution.
Propuestas de Proyectos Fin de Master
Propuestas 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.
