Sciweavers

CADE
2006
Springer
14 years 11 months ago
A Resolution-Based Decision Procedure for SHOIQ
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...
Yevgeny Kazakov, Boris Motik
CADE
2006
Springer
14 years 11 months ago
Tree Automata with Equality Constraints Modulo Equational Theories
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 ...
Florent Jacquemard, Laurent Vigneron, Michaël...
CADE
2006
Springer
14 years 11 months ago
Inferring Network Invariants Automatically
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...
Olga Grinchtein, Martin Leucker, Nir Piterman
CADE
2006
Springer
14 years 11 months ago
Automatic Termination Proofs in the Dependency Pair Framework
Jürgen Giesl, Peter Schneider-Kamp, Ren&eacut...
CADE
2006
Springer
14 years 11 months ago
Towards Self-verification of HOL Light
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 ...
John Harrison
CADE
2006
Springer
14 years 11 months ago
A Logical Characterization of Forward and Backward Chaining in the Inverse Method
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...
Kaustuv Chaudhuri, Frank Pfenning, Greg Price
CADE
2006
Springer
14 years 11 months ago
Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic
Abstract. Inspired by the Curry-Howard correspondence, we study normalisation procedures in the depth-bounded intuitionistic sequent calculus of Hudelmaier (1988) for the implicati...
Roy Dyckhoff, Delia Kesner, Stéphane Lengra...
CADE
2006
Springer
14 years 11 months ago
Verifying Mixed Real-Integer Quantifier Elimination
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...
Amine Chaieb
CADE
2006
Springer
14 years 11 months ago
Specifying and Reasoning About Dynamic Access-Control Policies
Access-control policies have grown from simple matrices to non-trivial specifications written in sophisticated languages. The increasing complexity of these policies demands corres...
Daniel J. Dougherty, Kathi Fisler, Shriram Krishna...