Category: Computer Science

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 , or a proof that none exist, i.e….


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…


What am I doing here? (My research topic)

Theory graph across formal libraries

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…