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

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

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