Baur, Michael (2023). Justification Logic, Semirings and Realizations. (Thesis). Universität Bern, Bern

Preview

Text 23baur_m.pdf - Thesis Available under License Creative Commons: Attribution (CC-BY 4.0). Download (642kB) | Preview

Abstract

The evidence terms in traditional justification logic have the form of polynomials, but semantically this structure is ignored by assigning a set of formulas to each term. We introduced the logic SE and the corresponding semantics, where terms are mapped to actual polynomials over a semiring. This gives a clear distinction between constants and variables, because constants in a term are mapped to elements in the semiring, yielding a function in the variables of the term. Further it is possible to compute with justifications. This can be used to model trust (Viterbi semiring), probabilities (powerset semiring), cost (tropical semiring), etc., depending on the chosen semiring. For the logic SE and its semantics we prove soundness and completeness. The completeness proof does not follow the standard line with maximal consistent sets. Instead we used a mapping to classical propositional logic, which basically replaces formulas of the form t : A by a fresh atomic proposition. Then we clarified the relationship between SE and the modal logic K by two realization theorems. The proof of the first one is closely related to a realization procedure without +, found by Kuznets. Then we considered ω-continuous semirings with the motivation that every Scott-continuous function on such a semiring has a fixed point, which can be used to establish a connection between common knowledge and justification logic. We therefore introduced the logic SEK with its semantics and proved soundness and completeness in a similar way as before. The main difference between SE and SEK is that the latter uses the polynomials over a semiring directly as justification terms. Apart from simplifying a lot this change was necessary for using the fixed points, because a fixed point is given by the (infinite) ascending Kleene chain, which would result in an infinite term. The infinite sum operation on the justification terms turned out to be too complex for common knowledge itself. For example terms for E0, E2, E4 and so on can be added to create a term for ΣnϵN E2n, which has no finite representation in common knowledge. We therefore introduced the system SAx (as an extension of common knowledge), which allows arbitrary sets of words of modal operators. Working towards a realization theorem we found a way of addressing occurrences of subformulas by a 0-1-sequence. This made the proof significantly more rigorous. When we dealt with the modus ponens rule we saw that all the applications of MP in a proof created a system of equations of the form x = f(x). We therefore used the fixed point theorem and got a realization algorithm that realizes the modus ponens rule directly and yields a normal realization. In the future it could be interesting to try to generalize this approach. By using fixed points one could find a realization procedure for more general modal fixed point logics including the modal μ-calculus.

Item Type:	Thesis
Dissertation Type:	Single
Date of Defense:	23 August 2023
Subjects:	000 Computer science, knowledge & systems 500 Science > 510 Mathematics
Institute / Center:	08 Faculty of Science > Institute of Computer Science (INF)
Depositing User:	Hammer Igor
Date Deposited:	22 Apr 2024 16:31
Last Modified:	23 Apr 2024 02:19
URI:	https://boristheses.unibe.ch/id/eprint/5035

Actions (login required)

View Item