CADE
2006
Springer
15 years 22 days ago
2006
Springer
CADE
2006
Springer
15 years 22 days 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
15 years 22 days ago
2006
Springer
CADE
2006
Springer
15 years 22 days 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
15 years 22 days 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
15 years 22 days 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
15 years 22 days 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
15 years 22 days 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
15 years 22 days 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
15 years 22 days 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 ...