CADE
2005
Springer
14 years 1 months ago
2005
Springer
We present the CoRe calculus for contextual reasoning which supports reasoning directly at the assertion level, where proof steps are justified in terms of applications of defini...
CADE
2005
Springer
14 years 5 months ago
2005
Springer
CADE
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. Pocket KRHyper is a reasoning system for Java-enabled mobile devices. The core of the system is a first order theorem prover and model generator based on the hyper table...
CADE
2005
Springer
14 years 5 months ago
2005
Springer
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...