Diferencia entre revisiones de «Proyectos relacionados»

De WikiGLC
Saltar a: navegación, buscar
(Proyectos de investigación)
(Proyectos de investigación)
Línea 2: Línea 2:
  
 
== Proyectos de investigación ==
 
== Proyectos de investigación ==
# [http://dream.inf.ed.ac.uk/projects/ontology_evolution/index.html Ontology Evolution in Physics]. (University of Edinburgh).
+
=== 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]. (University of Edinburgh).  
 
# [http://dream.inf.ed.ac.uk/projects/OntoEvolLaw/ Ontology Evolution in Law]. (University of Edinburgh).  
 
# [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]. (University of Edinburgh).
# [http://dream.inf.ed.ac.uk/projects/cog-mod/ A Cognitively Based Model of Theory Formulation and Reformulation] (University of Edinburgh).
+
# [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]. (University of Edinburgh).
 
# [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]. (University of Edinburgh).
 
# [http://dream.inf.ed.ac.uk/projects/critics/ Proof critics]. (University of Edinburgh).
 
# [http://dream.inf.ed.ac.uk/projects/critics/ Proof critics]. (University of Edinburgh).
# [http://dream.inf.ed.ac.uk/projects/mfotl/ Mechanising First-Order Temporal Logics]. (University of Edinburgh).
+
# [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)]. (University of Edinburgh).
+
# [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]. (University of Edinburgh).
+
# [http://www.cs.nott.ac.uk/~lad/research/nontheorems The Use of Proof in the Location of Programming Errors].
  
 
== Propuestas de Proyectos de Tesis Doctoral ==
 
== Propuestas de Proyectos de Tesis Doctoral ==

Revisión del 09:49 24 oct 2008

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

= Universidad de Edimburgo

  1. Ontology Evolution in Physics.
  2. Ontology Evolution in Law. (University of Edinburgh).
  3. The Integration and Interaction of Multiple Mathematical Reasoning Processes. (University of Edinburgh).
  4. A Cognitively Based Model of Theory Formulation and Reformulation
  5. Dynamic Ontology Refinement. (University of Edinburgh).
  6. Lakatos-style Reasoning. (University of Edinburgh).
  7. Proof critics. (University of Edinburgh).
  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.

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.

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, Fleuriot 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.