CADE
2006
Springer
14 years 4 months ago
2006
Springer
CADE
2006
Springer
14 years 4 months ago
2006
Springer
The HOL Light prover is based on a logical kernel consisting of about 400 lines of mostly functional OCaml, whose complete formal verification seems to be quite feasible. We would ...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Abstract. The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli's focusing strategy can be adap...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Abstract. Inspired by the Curry-Howard correspondence, we study normalisation procedures in the depth-bounded intuitionistic sequent calculus of Hudelmaier (1988) for the implicati...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Abstract. We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a wor...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Access-control policies have grown from simple matrices to non-trivial specifications written in sophisticated languages. The increasing complexity of these policies demands corres...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Abstract. We describe a second-order type theory with proof irrelevance. Within this framework, we give a representation of a form of Mac Lane set theory and discuss automated supp...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Church's Higher Order Logic is a basis for proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We ...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Abstract. In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisability problems ...