Hoven, Yvonne (2019) A Tableau Prover for Many-Valued Logics. Bachelor's Thesis, Artificial Intelligence.
|
Text
AI_BA_2019_YvonneHoven.pdf Download (676kB) | Preview |
|
Text
Toestemming.pdf Restricted to Registered users only Download (186kB) |
Abstract
A semantic tableau prover was implemented in Prolog for the following three many-valued logics: First Degree Entailment (FDE), (Strong) Kleene’s Logic (K3), and the Logic of Paradox (LP). These logics have one or two truth values more than classical logic, which only has the truth values true and false. The tableau rules for these three logics are similar, but differ in regard to their use of the non-classical truth values. The tableau prover uses the sound and complete tableau rules of the corresponding logics, and uses the same precedence hierarchy for the connectives as humans. The system was tested in a survey on interface and usability with regard to two types of proofs and counterexamples. In the first case, the proof tree was made with a depth-first approach, and the second proof tree was made with a breadth-first approach. In this survey, the breadth-first search proof was preferred. No examination of efficiency was done.
Item Type: | Thesis (Bachelor's Thesis) |
---|---|
Supervisor name: | Verbrugge, L.C. |
Degree programme: | Artificial Intelligence |
Thesis type: | Bachelor's Thesis |
Language: | English |
Date Deposited: | 12 Jul 2019 |
Last Modified: | 12 Jul 2019 11:53 |
URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/20143 |
Actions (login required)
View Item |