CADE
2006
Springer
14 years 12 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 12 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 12 months ago
2006
Springer
CADE
2006
Springer
14 years 12 months ago
2006
Springer
We define an interpretation of the Isabelle/HOL logic in HOL Light and its metalanguage, OCaml. Some aspects of the Isabelle logic are not representable directly in the HOL Light o...
CADE
2006
Springer
14 years 12 months ago
2006
Springer
We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correctness of our implementation of the subresulta...
CADE
2006
Springer
14 years 12 months ago
2006
Springer
Context Unification is the problem to decide for a given set of second-order equations E where all second-order variables are unary, whether there exists a unifier, such that for e...
CADE
2006
Springer
14 years 12 months ago
2006
Springer
Linear arithmetic decision procedures form an important part of theorem provers for program verification. In most verification benchmarks, the linear arithmetic constraints are dom...
CADE
2006
Springer
14 years 12 months ago
2006
Springer
Abstract. Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for ...
CADE
2006
Springer
14 years 12 months ago
2006
Springer
Abstract. We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of cat...
CADE
2006
Springer
14 years 12 months ago
2006
Springer
Abstract. Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far i...