Since I am now working with automated reasoning, I started to delve into the theory of classical resolution procedures. I decided to begin with an update of the constructive completeness proof of the resolution algorithm for classical propositional logic: see Github repo.