Javascript must be enabled for the correct page display

A Tableau Prover for Many-Valued Logics

Hoven, Yvonne (2019) A Tableau Prover for Many-Valued Logics. Bachelor's Thesis, Artificial Intelligence.


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

Download (186kB)


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 nameSupervisor E mail
Degree programme: Artificial Intelligence
Thesis type: Bachelor's Thesis
Language: English
Date Deposited: 12 Jul 2019
Last Modified: 12 Jul 2019 11:53

Actions (login required)

View Item View Item