How I convinced Isabelle that resolution is complete

Anders Schlichtkrull

Research output: Contribution to conferenceConference abstract for conferenceResearchpeer-review

103 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 201625 May 2016


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


Dive into the research topics of 'How I convinced Isabelle that resolution is complete'. Together they form a unique fingerprint.

Cite this