Thesis Topic Details
Topic ID: |
193 | |
Title: |
Proving theorems in and about epistemic logics in Isabelle and PVS | |
Supervisor: |
Kai Engelhardt | |
Research Area: |
Theory | |
| Associated Staff | ||
|---|---|---|
Assessor: |
Ron van der Meyden | |
| Topic Details | ||
Status: |
Active | |
Type: |
Research | |
Programs: |
CE CS SE | |
Group Suitable: |
Yes | |
Industrial: |
No | |
Pre-requisites: |
good understanding of mathematical logics | |
Description: |
The aim of this project is to build two competing proof assistant tools: one based on the theorem proving environment Isabelle (jointly developed by Cambridge and Munich Universities) and one based on the higher-order logic theorem prover PVS (developed by SRI in Stanford). Each of the proof assistants should help users in proving theorems in and about various epistemic logics (logics of knowledge or belief). It is currently unclear which theorem prover should be preferred for this application and why. A subgoal of this project is to evaluate the two suggested platforms for their respective suitability for the task at hand. One particularly interesting candidate logic would be the logic of local propositions (LLP) for multiple agents. LLP is the basis of an assertion language in a new refinement calculi currently developed. The (better one of the) proof assistants would form one corner stone of a future refinement assistant (similar to the B-Tool). | |
Comments: |
This project is advertised for a group of 2 students. It is possible to split it into two almost independent projects. The only mandatory collaboration would consist of writing a joint assessment of the merits not of their proof assistants but of the underlying theorem proving environments (Isabelle and PVS). | |
| Past Student Reports | ||
| No Reports Available. Contact the supervisor for more information.
Check out all available reports in the CSE Thesis Report Library. NOTE: only current CSE students can login to view and select reports to download. |
||