Spreading excellence and disseminating the cutting edge results of our research and development efforts is crucial to our institute. Check for our educational offers for Bachelor, Master and PhD studies at the University of Innsbruck!

Implementation of an Automated Theorem Prover for First-order Predicate Logics based on Partition-based Reasoning

Student name: 

Some years ago, there has been a proposal for a specific approach to Automated Theorem Proving in First-order predicate logic, called Partition-based Reasoning. The project aims at building a prototypical implementation and experimenting with different configurations of the system. An evaluation completes the project.
The aspects that should be covered by the project are the following: Description of Partition-based Reasoning, Implementation of a simple prototype for Partition-based Reasoning, Experimentation with different configurations of the systems (e.g. different consequence finding procedures for the single partitions), Optimization, Evaluation and summary of the experiments.