Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CADE
2005
Springer
11 years 16 days ago
The CoRe Calculus
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...
Serge Autexier
CADE
2005
Springer
11 years 4 months ago
Hierarchic Reasoning in Local Theory Extensions
Viorica Sofronie-Stokkermans
CADE
2005
Springer
11 years 4 months ago
KRHyper - In Your Pocket
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...
Alex Sinner, Thomas Kleemann
CADE
2005
Springer
11 years 11 months ago
The Decidability of the First-Order Theory of Knuth-Bendix Order
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...
Ting Zhang, Henny B. Sipma, Zohar Manna
CADE
2005
Springer
11 years 11 months ago
A Combination Method for Generating Interpolants
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...
Greta Yorsh, Madanlal Musuvathi
CADE
2005
Springer
11 years 11 months ago
On the Complexity of Equational Horn Clauses
Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentic...
CADE
2005
Springer
11 years 11 months ago
Nominal Techniques in Isabelle/HOL
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...
Christian Urban, Christine Tasson
CADE
2005
Springer
11 years 11 months ago
Deduction with XOR Constraints in Security API Modelling
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...
Graham Steel
CADE
2005
Springer
11 years 11 months ago
Regular Protocols and Attacks with Regular Knowledge
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...
Tomasz Truderung
books