CADE
2006
Springer
14 years 11 months ago
2006
Springer
Propositional canonical Gentzen-type systems, introduced in [1], are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly ...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlyi...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
One of the keys to the success of the TPTP and related projects is their consistent use of the TPTP language. The ability of the TPTP language to express solutions as well as probl...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
The nominal datatype package implements an infrastructure in Isabelle/HOL for defining languages involving binders and for reasoning conveniently about alpha-equivalence classes. P...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
Abstract. We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation. Is...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
This is a system description of the Description Logic reasoner FaCT++. The reasoner implements a tableaux decision procedure for the well known SHOIQ description logic, with additi...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
We investigate whether identification constraints such as keys and functional dependencies can be granted full status as a concept constructor in a Boolean-complete description log...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
In this paper, we discuss a lightweight approach to eliminate the overhead due to implicit type arguments during higher-order unification of dependently-typed terms. First, we show...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
It is well-known that the connection refinement of clause tableaux with paramodulation is incomplete (even with weak connections). In this paper, we present a new connection tablea...
CADE
2006
Springer
14 years 11 months ago
2006
Springer
We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Isabelle/HOL that have been recorded in HOL 4 or HOL-light a...