SAT Solving: DPLL, Clause Learning and Implication Graphs

This post is primarily directed at students in the AI class at University Erlangen to explain the Davis-Putnam (Logemann-Loveland) Algorithm for SAT solving and implication graphs for clause learning. The goal in a SAT problem is to find an assignment that satisfies a set of propositional formulae \( \Delta\), or a proof that none exist,…


Basics of Abstract Logic (Also: A Pointless but Fun, Correct and Complete Calculus for Divisibility)

This post is primarily directed at students in the AI class at University Erlangen to explain the basics, and in particular the formalism we use in the lectures, of abstract logic. In its (not actually, but for our purposes) most abstract form, a logical system consists of three things: A language \(\mathbb L\), i.e. a…


Meta-Meta-Tools and Theory Graphs (What is MMT?)

I work a lot with and on a particular piece of software called MMT, which was developed by Florian, so this is my attempt to explain what it does – which is not exactly easy, as you’ll see, but one of the things you can do with MMT is make computers (on some level) understand…


New Song – Bananifold

So, I finally managed to record the new song I promised here. The video is here: I figured I might try going a bit into detail, in case anyone’s interested – I’m not sure, why they should be, but who knows 🙂 The title Bananifold is a stupid math joke I like that started here…


An RPG magic system based on logic

(image source) One of our undergrad students recently finished his B.Sc. thesis on a serious game intended to teach the player to apply maths to real-world problems (this is probably going to be worth its own blog post, once the paper is publicly available somewhere), which got me thinking about other ways to teach math…


Why I tattooed Gödel on my arm

This is what the tattoo on my arm looks like (well – looked like right after I got it. You can still see the skin being noticably red/pale around it). It’s been designed by my flatmate at the time, Gwen. Without the arm it looks like this: Probably still not too legible, so let’s get…


What am I doing here? (My research topic)

In this post, I will try to explain what my Ph.D. is going to be about – of course, you can just read my proposal, but I assume that’s not really accessible to a lay-person. The broad topic is knowledge management across formal libraries, specifically libraries of formal mathematics obtained from (mostly) various computer-supported theorem…


How did I get here? (CV)

So, given that my CV is a bit more… non-linear than most people’s, I figured that might be worth a post on its own: I graduated (the german equivalent of) high school in Garmisch-Partenkirchen 2006, majoring in Math and English, at which point my plan was to study jazz guitar and make a living as…


Insert math as
Block
Inline
Additional settings
Formula color
Text color
#333333
Type math using LaTeX
Preview
\({}\)
Nothing to preview
Insert