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….
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…
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…
- Math Crankery with John Gabriel – “Cauchy’s Kludge”
- Math Crankery with John Gabriel – Calculus 102 (Cauchy Sequences and the Real Numbers)
- Math Crankery with John Gabriel – Calculus 101 (Convergence and Derivatives)
- Math Crankery with John Gabriel – The Dunning-Krüger Effect in a Nutshell
- SAT Solving: DPLL, Clause Learning and Implication Graphs