Schlichtkrull, A. (Participant)

Activity: Attending an eventParticipating in or organising workshops, courses, seminars etc.


Formalization of the Resolution Calculus for First-Order Logic

Speaker: Anders Schlichtkrull

Abstract: A formalization in Isabelle/HOL of the resolution calculus for first-order logic is presented. Its soundness and completeness are formally proven using the substitution lemma, semantic trees, Herbrand's theorem, and the lifting lemma. In contrast to previous formalizations of resolution, it considers first-order logic with full first-order terms, instead of the propositional case.

Talk "Formalization of the Resolution Calculus for First-Order Logic" at Club2 of the Chair for Logic and Verification at the Technical University of Munich
Period11 May 2016
Event typeSeminar