This post is primarily directed at students in the AI class at University Erlangen to explain the DavisPutnam (LogemannLoveland) 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…
Pages

Recent Posts
 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 DunningKrüger Effect in a Nutshell
 SAT Solving: DPLL, Clause Learning and Implication Graphs
Categories
Meta