CADE
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided in this process, but this ha...
CADE
2004
Springer
14 years 4 months ago
2004
Springer
We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.
CADE
2004
Springer
14 years 4 months ago
2004
Springer
Lambda logic is the union of first order logic and lambda calculus. We prove basic metatheorems for both total and partial versions of lambda logic. We use lambda logic to state a...
CADE
2004
Springer
14 years 4 months ago
2004
Springer
CADE
2004
Springer
14 years 4 months ago
2004
Springer
Deduction modulo is a theoretical framework for reasoning modulo a congruence on propositions. Computational steps are thus removed from proofs, thus allowing a clean separatation...