Preface: Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn Fairouz Kamareddine Preface Pages: 183 - 188
A Compendium of Continuous Lattices in MIZAR Grzegorz BancerekPiotr Rudnicki OriginalPaper Pages: 189 - 224
Automated Proof Construction in Type Theory Using Resolution Marc BezemDimitri HendriksHans de Nivelle OriginalPaper Pages: 253 - 275
External Rewriting for Skeptical Proof Assistants Quang Huy NguyenClaude KirchnerHélène Kirchner OriginalPaper Pages: 309 - 336
Algorithms and Proofs Inheritance in the FOC Language Virgile PrevostoDamien Doligez OriginalPaper Pages: 337 - 363