Section: Overall Objectives

Objectives

The team investigates applications of recent results in proof theory to the design of proof-checkers and automated theorem proving systems. It develops the Dedukti proof-checker and the iProver modulo and Zenon modulo automated theorem proving systems.