Javascript must be enabled for the correct page display

A tableau prover for GL provability logic

Loo, T. van (2017) A tableau prover for GL provability logic. Bachelor's Thesis, Artificial Intelligence.

AI_BA_2017_VanLoo.pdf - Published Version

Download (300kB) | Preview
[img] Text
Toestemming.pdf - Other
Restricted to Backend only

Download (79kB)


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

Actions (login required)

View Item View Item