Higher-Order Logic - DTU Compute - Denmark

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/