Licentiat Theses / Licentiatavhandlingar
https://hdl.handle.net/2077/25471
Sat, 20 Jul 2024 09:17:18 GMT2024-07-20T09:17:18ZComputational Content of Fixed Points
https://hdl.handle.net/2077/76018
Computational Content of Fixed Points
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.
Thu, 01 Dec 2022 00:00:00 GMThttps://hdl.handle.net/2077/760182022-12-01T00:00:00ZRepresentation matters in cyclic proof theory
https://hdl.handle.net/2077/75984
Representation matters in cyclic proof theory
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.
Sat, 01 Apr 2023 00:00:00 GMThttps://hdl.handle.net/2077/759842023-04-01T00:00:00ZModelling the logical mind - Using the cognitive architecture ACT-R to model human symbolic reasoning in the description logic 𝒜ℒℰ
https://hdl.handle.net/2077/74797
Modelling the logical mind - Using the cognitive architecture ACT-R to model human symbolic reasoning in the description logic 𝒜ℒℰ
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.
Sun, 01 Jan 2023 00:00:00 GMThttps://hdl.handle.net/2077/747972023-01-01T00:00:00ZMetamathematical fixed points
https://hdl.handle.net/2077/25513
Metamathematical fixed points
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.
Sun, 01 May 2011 00:00:00 GMThttps://hdl.handle.net/2077/255132011-05-01T00:00:00Z