How I convinced Isabelle that resolution is complete

Research output: Contribution to conferenceConference abstract for conferenceResearchpeer-review

52 Downloads (Pure)

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.
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
http://cadillac.compute.dtu.dk/

Workshop

WorkshopCADILLAC Workshop
LocationByens Lys Movie Theater, Fabriksområdet
CountryDenmark
CityCopenhagen
Period23/05/201125/05/2015
Internet address

Cite this

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