10 citations · 82 across the 40 of their papers we have counts for
7 papers · 1 filter
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…