TCS and PAM seminar

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

Description

Formalization of an Ordered Resolution Prover in Isabelle/HOL

Abstract:
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 reasoning.

Talk at the TCS and PAM seminar of the Theoretical Computer Science group at the Vrije Universiteit Amsterdam.
Period3 Nov 2017
Event typeSeminar
LocationAmsterdam, Netherlands