de Vries, Oscar (2018) A Tableau Prover for Non-Branching Transitive Temporal Logic with Density as Constraint. Bachelor's Thesis, Artificial Intelligence.
|
Text
AI_BA_2018_ODeVries.pdf Download (341kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
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 name: | Verbrugge, L.C. |
| Degree programme: | Artificial Intelligence |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 13 Apr 2018 |
| Last Modified: | 16 Apr 2018 09:45 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/16691 |
Actions (login required)
 |
View Item |