10 citations · 82 across the 40 of their papers we have counts for
43 papers
Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students
Merlin Carl
We describe two systems currently being developed that use large language models for the automatized correction of (i) exercises in translating back and forth between natural langu…
Improving the Diproche CNL through Autoformalization via Large Language Models
Merlin Carl
The Diproche system is an automated proof checker for texts written in a controlled fragment of German, designed for didactical applications in classes introducing students to proo…
Countable ranks at the first and second projective levels
Merlin Carl, Philipp Schlicht, Philip Welch
A rank is a notion in descriptive set theory that describes ranks such as the Cantor-Bendixson rank on the set of closed subsets of a Polish space, differentiability ranks on the s…
The strange world of transfinite Melodies -- Recognizability for weak and strong infinite time -register machines
Merlin Carl
For exponentially closed ordinals , we consider recognizability of constructible subsets of for -(w)ITRMs and their distribution in the constructible hierarchy. In partic…
Natural Language Proof Checking in Introduction to Proof Classes -- First Experiences with Diproche
Merlin Carl, Hinrich Lorenzen, Michael Schmitz
We present and analyze the employment of the Diproche system, a natural language proof checker, within a one-semester mathematics beginners lecture with 228 participants. The syste…
What is worthy of investigation? Philosophical attitudes and their impact on mathematical development by the example of discovering 10-adic numbers
Merlin Carl, Michael Schmitz
We describe in dialogue form a possible way of discovering and investigating 10-adic numbers starting from the naive question about a `largest natural number'. Among the topics we…
Lower bounds on and other properties of -ITRMs
Merlin Carl
This paper extends our paper \cite{C2} for the conference ``Computability in Europe'' 2022. After Infinite Time Turing Machines (ITTM) were introduced in Hamkins and Lewis \cite{HL…
Randomising Realisability
Merlin Carl, Lorenzo Galeotti, Robert Passmann
We consider a randomised version of Kleene's realisability interpretation of intuitionistic arithmetic in which computability is replaced with randomised computability with positiv…
Decision times of infinite computations
Merlin Carl, Philipp Schlicht, Philip Welch
The decision time of an infinite time algorithm is the supremum of its halting times over all real inputs. The decision time of a set of reals is the least decision time of an algo…
The Lost Melody Theorem for Infinite Time Blum-Shub-Smale Machines
Merlin Carl
We consider recognizability for Infinite Time Blum-Shub-Smale machines, a model of infinitary computability introduced in Koepke and Seyfferth [KS]. In particular, we show that the…
Realisability for Infinitary Intuitionistic Set Theory
Merlin Carl, Lorenzo Galeotti, Robert Passmann
We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). We show that our notion of OTM-realisability is sou…
Automatized Evaluation of Formalization Exercises in Mathematics
Merlin Carl
We describe two systems for supporting beginner students in acquiring basic skills in expressing statements in the formalism of first-order predicate logic; the first, called "math…
Number Theory and Axiomatic Geometry in the Diproche System
Merlin Carl
Diproche ("Didactical Proof Checking") is an automatic system for supporting the acquistion of elementary proving skills in the initial phase of university education in mathematics…
Resetting Infinite Time Blum-Shub-Smale-Machines
Merlin Carl, Lorenzo Galeotti
In this paper, we study strengthenings of Infinite Times Blum-Shub-Smale-Machines (ITBMs) that were proposed by Seyfferth in [14] and Welch in [15] obtained by modifying the behavi…
Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics
Merlin Carl
The Diproche system, an automated proof checker for natural language proofs specifically adapted to the context of exercises for beginner's students similar to the Naproche system…
Taming Koepke's Zoo II: Register Machines
Merlin Carl
We study the computational strength of resetting -register machines, a model of transfinite computability introduced by P. Koepke in \cite{K1}. Specifically, we prove the follow…
A Note on Clockability for Ordinal Turing Machines
Merlin Carl
We study clockability for Ordinal Turing Machines (OTMs). In particular, we show that, in contrast to the situation for ITTMs, admissible ordinals can be OTM-clockable, that $Σ_{2}…
Space and Time Complexity for Infinite Time Turing Machines
Merlin Carl
We consider notions of space complexity for Infinite Time Turing Machines (ITTMs) that were introduced by B. Löwe and studied further by J. Winter. We answer several open questions…
A Note on OTM-Realizability and Constructive Set Theories
Merlin Carl
We define an ordinalized version of Kleene's realizability interpretation of intuitionistic logic by replacing Turing machines with Koepke's ordinal Turing machines (OTMs), thus ob…
Effectivity and Reducibility with Ordinal Turing Machines
Merlin Carl
This article expands our work in [Ca16]. By its reliance on Turing computability, the classical theory of effectivity, along with effective reducibility and Weihrauch reducibility,…
A transfer principle for second-order arithmetic, and applications
Merlin Carl, Asgar Jamneshan
In the theory of conditional sets, many classical theorems from areas such as functional analysis, probability theory or measure theory are lifted to a conditional framework, often…
Reachability for infinite time Turing machines with long tapes
Merlin Carl, Benjamin Rin, Philipp Schlicht
Infinite time Turing machine models with tape length , denoted , strengthen the machines of Hamkins and Kidder [HL00] with tape length . A new phenomenon is that for som…
Some Observations on Infinitary Complexity
Merlin Carl
Continuing the study of complexity theory of Koepke's Ordinal Turing Machines (OTMs) that was started by Rin, Löwe and the author, we prove the following results: (1) An analogue o…
Canonical Truth
Merlin Carl, Philipp Schlicht
We introduce and study some variants of a notion of canonical set theoretical truth. By this, we mean truth in a transitive proper class model of ZFC that is uniquely character…