CADE
2001
Springer
14 years 4 months ago
2001
Springer
Proof assistants based on type theories, such as Coq and Lego, allow users to omit subterms on input that can be inferred automatically. While those mechanisms are well known, ad-h...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
We present a tool deciding a fragment of set theory. It is designed to be easily accessible via the internet and intuitively usable by anyone who is working with sets to describe a...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
The STRIP system is a theorem prover for intuitionistic propositional logic with two main characteristics: it deals with the duplication of formulae during proof-search from a fine...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
Abstract. This paper presents a technique for automated theorem proving with free variable tableaux that does not require backtracking. Most existing automated proof procedures usi...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
Context trees are a popular and effective tool for tasks such as compression, sequential prediction, and language modeling. We present an algebraic perspective of context trees for...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
Abstract. Nontrivial meta-complexity theorems, proved once for a programming language as a whole, facilitate the presentation and analysis of particular algorithms. This paper give...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
This paper investigates optimization techniques and data structures exploiting the use of so-called pseudo models. These techniques are applied to speed up TBox and ABox reasoning ...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
RACER implements a TBox and ABox reasoner for the logic SHIQ. RACER was the first full-fledged ABox description logic system for a very expressive logic and is based on optimized s...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
Canonical propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the subformula property, in...
CADE
2001
Springer
14 years 4 months ago
2001
Springer
The modalities of Dynamic Logic refer to the final state of a program execution and allow to specify programs with pre- and postconditions. In this paper, we extend Dynamic Logic w...