Short Description
This research project primarily aims at extending the Theorema system and establishing it as one of the state-of-the-art mathematical assistant systems. As such, it needs to provide both a concise, powerful and appealing inference kernel and user interface, as well as an extensive structured knowledge base of formalized mathematical theories that end-users can build upon. In this project, we plan to contribute to both aspects: On the system level, our intended research includes improving the automatic and interactive proving facilities of the system, equipping it with a type system, and adding further automation to the whole "theory exploration cycle". On the theory level, starting from the Theorema-formalization of reduction rings and Gröbner bases produced in the frame of our recent PhD thesis, we plan to formalize a novel approach to computing Gröbner bases by so-called generalized Sylvester matrices (or Macaulay matrices); this approach was first proposed by Bruno Buchberger and recently investigated thoroughly by Manuela Wiesinger-Widi in her PhD thesis.
Summarizing, the research project has five main objectives:
- Formalizing generalized Sylvester matrices: Formalize the theory of generalized Sylvester matrices (or Macaulay matrices), for computing Gröbner bases by matrix triangulation.
- Integrating interactive theorem proving into Theorema: Complement the existing purely automatic reasoning mode of the system by a convenient, easy-to-use, text-oriented interactive mode.
- Building correct inference systems: Implement a small kernel of basic inference methods and provide functions for easily coding high-level proof methods based on these basic inferences.
- Incorporating types into Theorema: Provide functionality for annotating Theorema-expressions with types, and employ type-checking and -inference for ensuring the logical correctness and -consistency of formal theories in Theorema.
- Automating theory exploration: Implement tools for automating certain frequently-occurring tasks in mathematical theory exploration, e.g. constructing quotient domains, defining inductive sets and -predicates, defining recursive functions, etc.
Contact
Alexander Maletzky
Research Institute for Symbolic Computation
Johannes Kepler University Linz
Altenberger Straße 69
A-4040 Linz, Austria
Phone: +43 (0)732 2468 9936
alexander.maletzky@risc.jku.at