CADE
2006
Springer
14 years 5 months ago
2006
Springer
We present a resolution-based decision procedure for the description logic SHOIQ--the logic underlying the Semantic Web ontology language OWL-DL. Our procedure is goal-oriented, an...
CADE
2006
Springer
14 years 5 months ago
2006
Springer
This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential ...
CADE
2006
Springer
14 years 5 months ago
2006
Springer
Abstract. Verification by network invariants is a heuristic to solve uniform verification of parameterized systems. Given a system P, a network invariant for P is that abstracts th...
CADE
2006
Springer
14 years 5 months ago
2006
Springer
CADE
2006
Springer
14 years 5 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 5 months ago
2006
Springer
CADE
2006
Springer
14 years 5 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 5 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 5 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 5 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...