Proyectos relacionados

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

1. Ontology Evolution in Physics. (University of Edinburgh).
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 (University of Edinburgh).
5. Dynamic Ontology Refinement. (University of Edinburgh).
6. [http://dream.inf.ed.ac.uk/projects/hrl/ Lakatos-style Reasoning

]. (University of Edinburgh).

1. Proof critics. (University of Edinburgh).
2. Mechanising First-Order Temporal Logics. (University of Edinburgh).
3. The Coral Project (finding counterexamples to false inductive conjectures). (University of Edinburgh).
4. The Use of Proof in the Location of Programming Errors. (University of Edinburgh).

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.