TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
Abstract. We present a generic approach to readable formal proof documents, called Intelligible semi-automated reasoning (Isar). It addresses the major problem of existing interact...
TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
The standard versions of HOL only support disjoint sums over finite families of types. This paper introduces disjoint sums over type classes containing possibly a countably infinit...
TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
Abstract. We describe the key features of the proof description language of Declare, an experimental theorem prover for higher order logic. We take a somewhat radical approach to p...
TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
Abstract. Intel is applying formal verification to various pieces of mathematical software used in Merced, the first implementation of the new IA-64 architecture. This paper discus...
TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
Gandalf is a first-order resolution theorem-prover, optimized for speed and specializing in manipulations of large clauses. In this paper I describe GANDALF TAC, a HOL tactic that ...
TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
Abstract. Isabelle/HOL has recently acquired new versions of definitional packages for inductive datatypes and primitive recursive functions. In contrast to its predecessors and mo...
TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We define the notion of a signature and of an algebra over a signature. ...
TPHOL
1999
IEEE
13 years 8 months ago
1999
IEEE
Combining theorem proving and model checking o ers the tantalizing possibility of e ciently reasoning about large circuits at high levels of abstraction. We have constructed a syst...