Licentiat Theses / Licentiatavhandlingar

Permanent URI for this collectionhttps://gupea-staging.ub.gu.se/handle/2077/25471

Browse

Recent Submissions

Now showing 1 - 4 of 4
  • No Thumbnail Available
    Item
    Computational Content of Fixed Points
    (2022-12) Barlucchi, Giacomo
    We study the computational content of fixed points in relation to two logical systems with distinct characteristics. Common to both research strands is a method for dealing with the iterative nature of fixed points. In the first part the interest is directed to a cyclic system ICA for intuitionistic arithmetic. The formal definition of the system is followed by the introduction of typed lambda-Y-calculus, whose terms represent the deductive process of cyclic proofs. A method for producing recursion schemes from instances of cyclic proofs is given. The result is a grammar whose language consists of lambda-terms, capturing the computational content implicit in the initial proof. In the second part, we look at the iteration of fixed points in terms of closure ordinals of formulas in the modal mu-calculus. A method for determining an upper bound on closure ordinals is presented and applied to formulas in fragments of the Sigma-1 class, with results that are in line with the already existing works. Annotated structures, to track how model changes affect the ordinals, and a pumping technique for these structures are the main tools used to establish an upper bound.
  • No Thumbnail Available
    Item
    Representation matters in cyclic proof theory
    (2023-04) Wehr, Dominik
    Cyclic proof systems allowderivations whose underlying structure is a finite graph, rather than a well-founded tree. The soundness of cyclic proofs is usually ensured by imposing additional conditions beyond well-formedness. Distinct cyclic representations of the same logic can be obtained by combining the same stock of logical rules with different soundness conditions. This thesis is a compilation of work in cyclic proof theory with a focus on the representation of cyclic proofs. The perspective is justified two-fold: First, the choice of representation of cyclic proofs has significant impact on proof theoretic investigations of cyclic proofs, dictating the effort required to derive desired results. Second, arguments which focus on the ‘cyclic’ aspects of cyclic proof systems, such as proof representations, rather than relying on specifics of logics, transfer more easily between different logics. This thesis makes several contributions to the field of cyclic proof theory. First, we present a method for generating reset proof systems, a representation of cyclic proofs which has previously been key to proof theoretic investigations, from cyclic proof systems with global trace conditions, by far the most common representation of cyclic proofs in the literature. Because the method is presented in a generic manner, this yields reset proof systems for most logics considered in the cyclic proof theory literature. Second, we transfer a proof method of the equivalence of cyclic and ‘inductive’ proof systems, first employed by Sprenger and Dam, to the setting of Heyting and Peano arithmetic. Whereas previous proofs of this equivalence for arithmetic theories have relied on intricate arithmetical formalisations of meta-mathematical concepts, our proof operates at the level of cyclic proof representations. Third, using insights into the aforementioned proof method, we put forward a novel form of representation for cyclic proof systems which is of interest to cyclic proof theory beyond the proving of cyclic-inductive equivalences.
  • No Thumbnail Available
    Item
    Modelling the logical mind - Using the cognitive architecture ACT-R to model human symbolic reasoning in the description logic 𝒜ℒℰ
    (2023) Fokkens Jelle, Tjeerd
    The problem of optimising automated explanations for entailments in knowledge bases is tackled by modelling deductive reasoning processes using the cognitive architecture ACT-R. This results in the model SHARP which simulates the algorithm for deciding inconsistency of an ABox in the description logic 𝒜ℒℰ as executed by a human. More precisely, SHARP enables predicting the inference time of this task, which is assumed to reflect cognitive load of a human agent. With the inference time, two complexity measures on ABoxes are defined that should correlate with cognitive load by design.
  • No Thumbnail Available
    Item
    Metamathematical fixed points
    (2011-05) Blanck, Rasmus
    This thesis concerns the concept of metamathematical fixed points. After an introduction, we survey the field of metamathematics, from la fin du siècle to present. We are especially interested in the notion of fixed points, theorems on the existence of various kinds of fixed points, and their applications to metamathematics. The second part of the thesis is a technical investigation of sets of fixed points. Given some recursively enumerable, consistent extension T of Peano arithmetic, we define for each formula θ(x) the set Fix^T (θ) := {δ : T |- δ ↔ θ(δ)}. Our main result on these sets is that they are all Σ_1-complete. Furthermore, we define for each formula θ(x), the set Fix_Γ^T (θ) := {δ : T |- δ ↔ θ(δ)}, where δ is a sentence in Γ. Using methods of Bennet, Bernardi, Guaspari, Lindström, and Smullyan, we characterise these sets for formulas in Γ' ⊃ Γ, and provide partial results for formulas in Γ. We give a sufficient condition on recursive sets to be a set of fixed points, and show that such sets exists. We also present a sufficient condition for a recursively enumerable set of Γ-sentences to be a set of fixed points of a Γ-formula. In the following section, we study the structure of sets of fixed points ordered under set inclusion, and prove certain properties on these structures. Finally, we connect our research to another open problem of metamathematics, and state some possible further work.