Perin, Francesca (2019) Implementing Maehara's method for star-free Propositional Dynamic Logic. Bachelor's Thesis, Artificial Intelligence.
|
Text
Bachelor_s_Thesis_s2865300_PerinFrancesca.pdf Download (289kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (141kB) |
Abstract
Craig’s interpolation theorem has been proven for different logics such as first-order logic, propositional and basic modal logic. However, it is still an open debate whether PropositionalDynamic Logic (PDL) has said property. This research does not aim to close such debate. Our goal is to implement an interpolation prover for propositional logic, basic modal logic, some of its extensions, up to star-free PDL. Our program randomly generates an implication and then the prover determines its validity by using sequent calculus. The prover then, given the valid sentence, also finds an interpolant using Maehara’s partition interpolation method. The prover then outputs the sequent calculus proof and the computed interpolant. For propositional logic, all rules of inference and the computation of the interpolant are fully deterministic. For modal logic and star-free PDL, some of the rules are non-deterministic in which case the prover uses depth-first search to find one of the valid proofs. The prover is tested with 450.000 randomly generated formulas and also a specific set of formulas for all logics. For each randomly generated formula tested that was found valid a final interpolant which respected the definition was found. This was also the case for the specific set, only one formula was supposed to be non-valid but was found to be valid. We argue that this was due to a mistake as the proof for that formula is correct.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Gattinger, B.R.M. |
| Degree programme: | Artificial Intelligence |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 26 Aug 2019 |
| Last Modified: | 27 Aug 2019 10:38 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/20770 |
Actions (login required)
 |
View Item |