Loo, T. van (2017) A tableau prover for GL provability logic. Bachelor's Thesis, Artificial Intelligence.
|
Text
AI_BA_2017_VanLoo.pdf - Published Version Download (300kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf - Other Restricted to Backend only Download (79kB) |
Abstract
A simple tableau prover using sound and complete tableau-rules for the provability logic GL was implemented in C using a priority queue for the application of rules. Two types of substitutions were tested, the first substitutes each operator but the box, negation, and disjunction, and the second converts the input to negation normal form. For some input sentences, the tableau and time become shorter after substitution, where for some others it increases exponentially. Although the program typically runs in the order of magnitude microseconds for simple tableaux, the lack of benchmark sets for GL as well as some hardware limitations make the results ungeneralisable.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Degree programme: | Artificial Intelligence |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 15 Feb 2018 08:29 |
| Last Modified: | 15 Feb 2018 08:29 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/15402 |
Actions (login required)
 |
View Item |