Javascript must be enabled for the correct page display

Investigating the Shape of Tableaux in RM3 and L3

van Leeuwen, Ludi (2019) Investigating the Shape of Tableaux in RM3 and L3. Bachelor's Thesis, Artificial Intelligence.


Download (335kB) | Preview
[img] Text
Restricted to Registered users only

Download (139kB)


Solving logical inferences by hand is not the most efficient way of doing logic. An automated theorem prover can help generate tableau proofs and countermodels for different logics. This automation can make it possible to investigate the structure of tableaux on a larger scale. Investigating differences between structures can be done by looking at the edit distance: the number of changes that need to be made in order to transform one structure into the other. By applying edit distances to tableaux for L3 and RM3, as generated by an automatic tableaux solver, the causes of differences in structures of tableaux can be investigated. The differences in structure arise from the different closing rules and the different interpretations of the conditional in both logics.

Item Type: Thesis (Bachelor's Thesis)
Supervisor nameSupervisor E mail
Degree programme: Artificial Intelligence
Thesis type: Bachelor's Thesis
Language: English
Date Deposited: 27 Aug 2019
Last Modified: 27 Aug 2019 10:23

Actions (login required)

View Item View Item