CADE
2006
Springer
15 years 22 days ago
2006
Springer
Abstract. We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus ...
CADE
2006
Springer
15 years 22 days ago
2006
Springer
CEL (Classifier for EL) is a reasoner for the small description logic EL+ which can be used to compute the subsumption hierarchy induced by EL+ ontologies. The most distinguishing ...
CADE
2006
Springer
15 years 22 days ago
2006
Springer
We introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a (...
CADE
2006
Springer
15 years 22 days ago
2006
Springer
In this paper we introduce several new improvements to the bottom-up model generation (BUMG) paradigm. Our techniques are based on non-trivial transformations of first-order probl...