CADE
2004
Springer
14 years 11 months ago
2004
Springer
We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.
CADE
2004
Springer
14 years 11 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 11 months ago
2004
Springer
CADE
2004
Springer
14 years 11 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...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
Two kinds of orderings are widely used in term rewriting and theorem proving, namely recursive path ordering (RPO) and Knuth-Bendix ordering (KBO). They provide powerful tools to p...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
We present a combination method for generating interpolants for a class of first-order theories. Using interpolant-generation procedures for individual theories as black-boxes, our...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
CADE
2005
Springer
14 years 11 months ago
2005
Springer
Abstract This paper describes a formalisation of the lambda-calculus in a HOL-based theorem prover using nominal techniques. Central to the formalisation is an inductive set that i...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
We introduce XOR constraints, and show how they enable a theorem prover to reason effectively about security critical subsystems which employ bitwise XOR. Our primary case study is...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
We prove that, if the initial knowledge of the intruder is given by a deterministic bottom-up tree automaton, then the insecurity problem for cryptographic protocols with atomic ke...