TCS and PAM seminar
We have a weekly informal seminar of the TCS group,
jointly with the
PAM-seminar from CWI,
often but not always on Fridays 15.30 - 16.30 at the VU.
Femke van Raamsdonk
(e: f.van.raamsdonk at vu.nl) if you wish to give a talk.
2017 11 03 (Friday)
Anders Schlichtkrull (Technical University of Denmark)
Formalization of an Ordered Resolution Prover in Isabelle/HOL
This is joint work with Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann.
We present a formalization of the first half of Bachmair and Ganzinger's
chapter on resolution theorem proving in Isabelle/HOL, culminating with a
refutationally complete first-order prover based on ordered resolution with
literal selection. We develop general infrastructure and methodology that can
form the basis of completeness proofs for related calculi (e.g.,
superposition). Our work clarifies several fine points in the chapter's text,
emphasizing the value of formal proofs in the field of automated
for a list of previous seminars.
Last modified November 3, 2017.