CADE
2006
Springer
14 years 4 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 4 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 4 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 4 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 4 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 4 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 4 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...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
We present a proof procedure that is complete for first-order logic, but which can also be used when searching for finite models. The procedure uses a normal form which is based on...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
We present a verified enumeration of tame graphs as defined in Hales' proof of the Kepler Conjecture and confirm the completeness of Hales' list of all tame graphs while ...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
