Activity: Attending an event › Participating 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