Diferencia entre revisiones de «Proyectos relacionados»

De WikiGLC
Saltar a: navegación, buscar
(→‎Proyectos de investigación)
 
(No se muestran 12 ediciones intermedias del mismo usuario)
Línea 2: Línea 2:
  
 
== Proyectos de investigación ==
 
== Proyectos de investigación ==
−
=== Universidad de Edimburgo ==
+
=== 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/ontology_evolution/index.html Ontology Evolution in Physics].
−
# [http://dream.inf.ed.ac.uk/projects/OntoEvolLaw/ Ontology Evolution in Law]. (University of Edinburgh).  
+
# [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]. (University of Edinburgh).
+
# [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/cog-mod/ A Cognitively Based Model of Theory Formulation and Reformulation].
−
# [http://dream.inf.ed.ac.uk/projects/dor/ Dynamic Ontology Refinement]. (University of Edinburgh).
+
# [http://dream.inf.ed.ac.uk/projects/dor/ Dynamic Ontology Refinement].
−
# [http://dream.inf.ed.ac.uk/projects/hrl/ Lakatos-style Reasoning]. (University of Edinburgh).
+
# [http://dream.inf.ed.ac.uk/projects/hrl/ Lakatos-style Reasoning].
−
# [http://dream.inf.ed.ac.uk/projects/critics/ Proof critics]. (University of Edinburgh).
+
# [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/mfotl/ Mechanising First-Order Temporal Logics].
 
# [http://dream.inf.ed.ac.uk/projects/coral/ The Coral Project (finding counterexamples to false inductive conjectures)].
 
# [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://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 ==
 
== Propuestas de Proyectos de Tesis Doctoral ==
Línea 21: Línea 37:
 
# 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].
 +
# F. Wiedijk [http://www.cs.ru.nl/~freek/projects/ Lista de proyectos de formalización].
  
 
== Propuestas de Proyectos Fin de Master ==
 
== Propuestas de Proyectos Fin de Master ==
Línea 30: Línea 47:
 
# 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, Fleuriot [http://homepages.inf.ed.ac.uk/mcryan/projs0809/project.php?number=P033 A PRESS Package for Isabelle].
+
# 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 13: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.

Proyectos de investigación

INRIA Sophia-Antipolis

  1. Galapagos (apply computerized theorem proving to geometry).

Universidad de Edimburgo

  1. Ontology Evolution in Physics.
  2. Ontology Evolution in Law.
  3. The Integration and Interaction of Multiple Mathematical Reasoning Processes.
  4. A Cognitively Based Model of Theory Formulation and Reformulation.
  5. Dynamic Ontology Refinement.
  6. Lakatos-style Reasoning.
  7. Proof critics.
  8. Mechanising First-Order Temporal Logics.
  9. The Coral Project (finding counterexamples to false inductive conjectures).
  10. The Use of Proof in the Location of Programming Errors.
  11. Formal Verification in Computational Geometry.
  12. MATHsAiD - Automatically generating mathematical theorems.
  13. Quantomatic Automated Reasoning for Quantum Computations].
  14. MathServe a framework for integrating reasoning systems as Web Services.
  15. PG Tips: A Recommender System for an Interactive Theorem Prover.
  16. Anastasia a functional programming editor that uses formal verification].

Universidad de la Rioja

  1. reKenzo.
    El objetivo es facilitar la interacción remota con el sistema Kenzo de topología algebraica.

Universidad de Liverpool

  1. Composing and decomposing ontologies: a logic-based approach.

Propuestas de Proyectos de Tesis Doctoral

  1. A. Bundy A Proof Management Tool.
  2. A. Bundy A Programming by Analogy Editor for Godel.
  3. A. Bundy A Teaching Aid for Nonstandard Analysis.
  4. A. Bundy Synthesis of Decision Procedures.
  5. A. Bundy Automatic Hardware Verification.
  6. A. Bundy Ontology Evolution.
  7. F. Wiedijk Lista de proyectos de formalización.

Propuestas de Proyectos Fin de Master

  1. A. Bundy 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

  1. A. Bundy An elementary, machine assisted proof of a multilinear generalisation of the Cauchy-Schwarz inequality.
  2. A. Bundy Heuristic Measures for Controlling Proof Search in a Model Elimination Prover.
  3. A. Bundy Recommender system for an interactive theorem prover.
  4. J. Fleuriot Mechanical Verification in Isabelle using Powerlists.
  5. J, FleurProiot A PRESS Package for Isabelle.
  6. J. Fleuriot Experiments in Formalized Mathematics: More Integration Theory in Isabelle/HOL.
  7. I. Stark Machine formalization of the continuous pi-calculus.

Otras propuestas

  1. Propuestas de proyectos de Amine Chaieb.
Obtenido de «https://www.glc.us.es/web/index.php?title=Proyectos_relacionados&oldid=609»