Speaker:
Anders Schlichtkrull
 
Title:
How I convinced Isabelle that resolution is complete
 
Abstract:
Isabelle is a proof assistant, i.e., a computer program that can help its user conduct proofs and check their correctness. In this talk I motivate the use of proof assistants, and I explain how I used Isabelle to prove a logical system, the resolution calculus, sound and complete.