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.

Getting Started with Isabelle

IsaFoL: Isabelle Formalization of Logic

Proof Assistants and Related Tools - The PART Project

NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle


Photo: Jørgen Villadsen

Jørgen Villadsen 2017-11-12 http://hol.compute.dtu.dk/