My PhD work is centered around automated theorem proving in first-order logic. This is obviously a very cool topic (otherwise I wouldn't have focused on it), so this post is a crash course (but the program won't crash because I use OCaml) on one of the most classic method to prove (some) theorems automatically. I named... resolution! The goal is to prove some (not too complicated) theorems automatically. In other words, we want a program that reads a bunch of axioms and a formula that we conj...
