Sciweavers

ISCIS
2004
Springer
13 years 10 months ago
Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL
This paper presents a machine-checked proof of the Basic Theorem on Concept Lattices, which appears in the book “Formal Concept Analysis” by Ganter and Wille, in the Isabelle/H...
Baris Sertkaya, Halit Oguztüzün
CADE
2004
Springer
14 years 5 months ago
Formalizing O Notation in Isabelle/HOL
We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.
Jeremy Avigad, Kevin Donnelly