Javascript must be enabled for the correct page display

A Tableau Prover for Non-Branching Transitive Temporal Logic with Density as Constraint

de Vries, Oscar (2018) A Tableau Prover for Non-Branching Transitive Temporal Logic with Density as Constraint. Bachelor's Thesis, Artificial Intelligence.

[img]
Preview
Text
AI_BA_2018_ODeVries.pdf

Download (341kB) | Preview
[img] Text
toestemming.pdf
Restricted to Registered users only

Download (73kB)

Abstract

This research aims to build a tableau-based prover for Temporal Logic. Constraints to this logic are that its models must be transitive, dense and non-branching towards the future and past. An algorithm was built in Python using a priority queue for the application of tableaurules. Additionally the logic is proven to be sound and complete with regards to these constraints. The algorithm creates a readable human-like tableau to check the validity of input inferences. For invalid inferences, a counter-model is provided in the output. The combination of density, which can theoretically be applied infinitely many times, together with non-branching causes run-times to increase exponentially for certain inputs.

Item Type: Thesis (Bachelor's Thesis)
Supervisor:
Supervisor nameSupervisor E mail
Verbrugge, L.C.L.C.Verbrugge@rug.nl
Degree programme: Artificial Intelligence
Thesis type: Bachelor's Thesis
Language: English
Date Deposited: 13 Apr 2018
Last Modified: 16 Apr 2018 09:45
URI: http://fse.studenttheses.ub.rug.nl/id/eprint/16691

Actions (login required)

View Item View Item