CADE
2008
Springer
14 years 11 months ago
2008
Springer
Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics with various applications in computer scienc...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. We consider the problem of computing the logical difference between distinct versions of description logic terminologies. For the lightweight description logic EL, we pre...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. Tableau calculi are the state-of-the-art for reasoning in description logics (DL). Despite recent improvements, tableau-based reasoners still cannot process certain knowl...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. We present the first terminating tableau calculus for basic hybrid logic with the difference modality and converse modalities. The language under consideration is basic m...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
CADE
2008
Springer
14 years 11 months ago
2008
Springer
In this paper, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. This method is easy to implement, but si...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. This paper presents verified quantifier elimination procedures for dense linear orders (DLO), for real and for integer linear arithmetic. The DLO procedures are new. All ...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Interval-based methods are commonly used for computing numerical bounds on expressions and proving inequalities on real numbers. Yet they are hardly used in proof assistants, as th...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. The application area of security protocols raises several problems that are relevant to automated deduction. We describe in this note some of these challenges.