How I convinced Isabelle that resolution is complete

Research output: Contribution to conferenceConference abstract for conferenceResearchpeer-review

52 Downloads (Pure)


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.
Original languageEnglish
Publication date2016
Number of pages1
Publication statusPublished - 2016
EventCADILLAC Workshop - Byens Lys Movie Theater, Fabriksområdet, Copenhagen, Denmark
Duration: 23 May 201125 May 2015


WorkshopCADILLAC Workshop
LocationByens Lys Movie Theater, Fabriksområdet
Internet address

Cite this

Schlichtkrull, A. (2016). How I convinced Isabelle that resolution is complete. Abstract from CADILLAC Workshop, Copenhagen, Denmark.