Portal for research and teaching in higher-order logic, in particular using the proof assistant Isabelle for formalization and verification.
Talk on Friday 18 December 2015 11:00-12:00 at DTU Lyngby Campus, Building 321, Room 033
Soundness and Completeness Proofs by Coinductive Methods
By Dmitriy Traytel, Information Security Group, ETH Zurich
Abstract: Coinductive methods can produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. The results are formalized in the proof assistant Isabelle using the recently introduced support for codatatypes and corecursion. In the talk I will focus on the abstract core of a classical completeness result: a property of possibly infinite derivation trees. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of first-order logic. All of this is joint work with Jasmin Blanchette and Andrei Popescu.
Hosts: Anders Schlichtkrull & Jørgen Villadsen, DTU Compute, AlgoLoG Section
Getting Started with Isabelle
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
Proof Assistants and Related Tools - The PART Project
IsaFoL: Isabelle Formalization of Logic
SimPro: Simple Prover - With a Formalization in Isabelle
Jørgen Villadsen 2015-12-12 http://hol.compute.dtu.dk/