Welcome to Machine Logic!
[general This blog will cover a variety of topics connected with automated theorem proving and its applications, such as computer system verification and formalised mathematics. It’s aimed at readers who have some grasp of formal proofs already, perhaps from an undergraduate course on discrete mathematics or symbolic logic. There will be tutorial posts on such mysteries as LCF, intuitionism and inductive reasoning. Many posts will be overviews of work published elsewhere, so this blog will also function as a shop window into the vast literature on computational logic.
The focus here will naturally be the work of my research group at Cambridge, so much of the material will relate to the proof assistant Isabelle/HOL and the millions of lines of formalised mathematics in the Archive of Formal Proofs. However, guest posts on appropriate topics are welcome, regardless of perspective.