Sciweavers

Share
CADE
2003
Springer
9 years 7 months ago
The CADE-19 ATP System Competition
Geoff Sutcliffe, Christian B. Suttner
CADE
2003
Springer
9 years 7 months ago
Subset Types and Partial Functions
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...
Aaron Stump
CADE
2003
Springer
9 years 7 months ago
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular propertie...
Renate A. Schmidt, Ullrich Hustadt
CADE
2003
Springer
9 years 7 months ago
Optimizing Higher-Order Pattern Unification
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...
Brigitte Pientka, Frank Pfenning
CADE
2003
Springer
9 years 7 months ago
Equational Abstractions
José Meseguer, Miguel Palomino, Narciso Mar...
CADE
2003
Springer
9 years 7 months ago
Proving Pointer Programs in Higher-Order Logic
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...
Farhad Mehta, Tobias Nipkow
CADE
2003
Springer
9 years 7 months ago
Algorithms for Ordinal Arithmetic
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...
Panagiotis Manolios, Daron Vroon
CADE
2003
Springer
9 years 7 months ago
Canonization for Disjoint Unions of Theories
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...
Sava Krstic, Sylvain Conchon
CADE
2003
Springer
9 years 7 months ago
TRP++2.0: A Temporal Resolution Prover
Ullrich Hustadt, Boris Konev
books