CADE
2003
Springer
14 years 4 months ago
2003
Springer
CADE
2003
Springer
14 years 4 months ago
2003
Springer
A classical higher-order logic PFsub of partial functions is defined. The logic extends a version of Farmer's logic PF by enriching the type system of the logic with subset ty...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular propertie...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
Abstract. We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
CADE
2003
Springer
14 years 4 months ago
2003
Springer
CADE
2003
Springer
14 years 4 months ago
2003
Springer
This paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
Ordinals form the basis for termination proofs in ACL2. Currently, ACL2 uses a rather inefficient representation for the ordinals up to 0 and provides limited support for reasoning...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
If there exist efficient procedures (canonizers) for reducing terms of two first-order theories to canonical form, can one use them to construct such a procedure for terms of the d...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
