Diferencia entre revisiones de «Proyectos relacionados»
(→Propuesta de Proyectos de Tesis Doctoral) |
|||
| (No se muestran 19 ediciones intermedias del mismo usuario) | |||
| 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 == | ||
| + | === INRIA Sophia-Antipolis === | ||
| + | # [http://galapagos.gforge.inria.fr/ Galapagos] (apply computerized theorem proving to geometry). | ||
| + | |||
| + | === Universidad de Edimburgo === | ||
| + | # [http://dream.inf.ed.ac.uk/projects/ontology_evolution/index.html Ontology Evolution in Physics]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/OntoEvolLaw/ Ontology Evolution in Law]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/platform-07-11/ The Integration and Interaction of Multiple Mathematical Reasoning Processes]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/cog-mod/ A Cognitively Based Model of Theory Formulation and Reformulation]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/dor/ Dynamic Ontology Refinement]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/hrl/ Lakatos-style Reasoning]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/critics/ Proof critics]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/mfotl/ Mechanising First-Order Temporal Logics]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/coral/ The Coral Project (finding counterexamples to false inductive conjectures)]. | ||
| + | # [http://www.cs.nott.ac.uk/~lad/research/nontheorems The Use of Proof in the Location of Programming Errors]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/fvcg/ Formal Verification in Computational Geometry]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/mathsaid MATHsAiD - Automatically generating mathematical theorems]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/quantomatic Quantomatic] Automated Reasoning for Quantum Computations]. | ||
| + | # [http://www.ags.uni-sb.de/~jzimmer/mathserve.html MathServe] a framework for integrating reasoning systems as Web Services. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/RecommenderSystem PG Tips: A Recommender System for an Interactive Theorem Prover]. | ||
| + | # [http://dream.inf.ed.ac.uk/projects/anastasia Anastasia] a functional programming editor that uses formal verification]. | ||
| + | |||
| + | === Universidad de la Rioja === | ||
| + | # [http://www.unirioja.es/cu/joheras reKenzo]. | ||
| + | #: El objetivo es facilitar la interacción remota con el sistema Kenzo de topología algebraica. | ||
| + | |||
| + | === Universidad de Liverpool === | ||
| + | # [http://www.csc.liv.ac.uk/~dirk/modularity/ Composing and decomposing ontologies: a logic-based approach]. | ||
| + | |||
| + | == 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/cynthia-prolog.html A Programming by Analogy Editor for Godel]. | ||
| + | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/nsa.html A Teaching Aid for Nonstandard Analysis]. | ||
| + | # A. Bundy [http://homepages.inf.ed.ac.uk/bundy/projects/phd/phd-project-dec-proc.html Synthesis of Decision Procedures]. | ||
| + | # 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]. | ||
| + | # F. Wiedijk [http://www.cs.ru.nl/~freek/projects/ Lista de proyectos de formalización]. | ||
| + | |||
| + | == 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=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]. | # 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, | + | # J, FleurProiot [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]. | # 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]. | # I. Stark [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P162 Machine formalization of the continuous pi-calculus]. | ||
| − | == | + | == Otras propuestas == |
| − | # | + | # [http://www.cl.cam.ac.uk/~ac638/students/sp.html Propuestas de proyectos de Amine Chaieb]. |
| − | + | [[Category:Projects]] | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
Revisión actual del 12:12 21 ene 2009
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
INRIA Sophia-Antipolis
- Galapagos (apply computerized theorem proving to geometry).
Universidad de Edimburgo
- Ontology Evolution in Physics.
- Ontology Evolution in Law.
- The Integration and Interaction of Multiple Mathematical Reasoning Processes.
- A Cognitively Based Model of Theory Formulation and Reformulation.
- Dynamic Ontology Refinement.
- Lakatos-style Reasoning.
- Proof critics.
- Mechanising First-Order Temporal Logics.
- The Coral Project (finding counterexamples to false inductive conjectures).
- The Use of Proof in the Location of Programming Errors.
- Formal Verification in Computational Geometry.
- MATHsAiD - Automatically generating mathematical theorems.
- Quantomatic Automated Reasoning for Quantum Computations].
- MathServe a framework for integrating reasoning systems as Web Services.
- PG Tips: A Recommender System for an Interactive Theorem Prover.
- Anastasia a functional programming editor that uses formal verification].
Universidad de la Rioja
- reKenzo.
- El objetivo es facilitar la interacción remota con el sistema Kenzo de topología algebraica.
Universidad de Liverpool
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.
- F. Wiedijk Lista de proyectos de formalización.
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, FleurProiot 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.
