Implementing analytic tableaux for justification logic
dc.rights.license | CC-BY-NC-ND | |
dc.contributor.advisor | Iemhoff, R. | |
dc.contributor.advisor | Prakken, H. | |
dc.contributor.author | Steenbergen, N. | |
dc.date.accessioned | 2018-06-25T17:01:32Z | |
dc.date.available | 2018-06-25T17:01:32Z | |
dc.date.issued | 2018 | |
dc.identifier.uri | https://studenttheses.uu.nl/handle/20.500.12932/29178 | |
dc.description.abstract | This Master's thesis presents new decidable tableau systems for the justification logics J and LP, and proves their soundness and completeness by providing a proof of cut-elimination. The accompanying Haskell software, "judge", is able to automatically construct tableaux for any tableau systems defined by the user, including the proposed system. The crux lies in its ability to deal with systems in which the expansion rules may introduce formulas that are not subterms of formulas that previously occurred on the branch. | |
dc.description.sponsorship | Utrecht University | |
dc.format.extent | 820903 | |
dc.format.extent | 47302 | |
dc.format.mimetype | application/pdf | |
dc.format.mimetype | application/x-gzip | |
dc.language.iso | en | |
dc.title | Implementing analytic tableaux for justification logic | |
dc.type.content | Master Thesis | |
dc.rights.accessrights | Open Access | |
dc.subject.keywords | logic, formal logic, justification logic, justification, logic of proofs, tableau, method of analytic tableaux, epistemic, knowledge, belief, provability, satisfiability, validity, consistency, proof search, theorem proving, decision procedure, decidability, subformula property, soundness, completeness, proof tree, evidence, complexity, haskell, implementation, program, software, tool, application, derivation, formula | |
dc.subject.courseuu | Artificial Intelligence |