activity
20152022
most citedNatural Language Proof Checking in Introduction to Proof Classes -- First Experiences with Diproche

5 citations · 8 across the 7 of their papers we have counts for

collaborators

10 papers

cs.LO20225 cited

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…

math.NT2021

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…

math.LO2021

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…

math.LO2020

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…

math.LO2020

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…

math.LO2020

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…