SET THEORY FOR VERIFICATION II: INDUCTION AND RECURSION
Lawrence C. Paulson
ABSTRACT: A theory of recursive definitions has been mechanized
in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective
is to support the formalization of particular recursive definitions
for use in verification, semantic proofs, and other computational
reasoning.
{\it Inductively defined sets} are expressed as least fixedpoints,
applying the Knaster-Tarski theorem over a suitable set.
{\it Recursive functions} are defined by well-founded recursion
and its derivatives, such as transfinite recursion. {\it Recursive
data structures} are expressed by applying the Knaster-Tarski
theorem to a set, such as $V_\omega$ that is closed under Cartesian
product and disjoint sum.
Worked examples include the transitive closure of a relation, lists,
variable-branching trees, and mutually recursive trees and forests.
The Schr\"{o}der-Bernstein theorem and the soundness of
propositional logic are proved in Isabelle sessions.
A RAMSEY THEOREM IN BOYER-MOORE LOGIC
by Kenneth Kunen
ABSTRACT: We use the Boyer-Moore Prover, Nqthm, to verify the
Paris-Harrington version of Ramsey's theorem. The proof we verify
is a modification of the one given by Ketonen and Solovay.
The theorem is not provable in Peano Arithmetic, and one key
step in the proof requires $\epsilon_0$ induction.
THE ANATOMY OF VAMPIRE
Implementing Bottom-up Procedures with Code Trees
by Andrei Voronkov
ABSTRACT: We present an implementation technique for a class of
bottom-up logic procedures. The technique is based on {\it code trees}.
It is intended to speed up most important and costly operations,
such as subsumption and resolution. As an example, we consider
the forward subsumption problem which is the bottleneck of many
systems implementing first-order logic.
To efficiently implement subsumption, we specialize subsumption
algorithms at run time, using the {\it abstract subsumption
machine.} The abstract subsumption machine makes subsumption-check
using sequences of instructions that are similar to the WAM
instructions. It gives an efficient implementation of the
"clause at a time" subsumption problem. To implement subsumption
on the "set at a time" basis, we combine sequences of instructions
in {\it code trees.}
We show that this technique yields a new way of indexing classes.
Some experimental results are given.
The code trees technique may be used in various procedures,
including binary resolution, hyper-resolution, UR-resolution, the
inverse method, paramodulation and rewriting, OLDT-resolution,
SLD-AL-resolution, bottom-up evaluation of logic programs, and
disjunctive logic programs.
A NOTE ON ASSUMPTIONS ABOUT SKOLEM FUNCTIONS
by Hans J\"{o}rgen Ohlbach and Christoph Weidenbach
ABSTRACT: Skolemization is not an equivalence preserving
transformation. For the purposes of refutational theorem
proving it is sufficient that skolemization preserves
satisfiability and unsatisfiability. Therefore there is
sometimes some freedom in interpreting Skolem functions in
a particular way. We show that in certain cases it is
possible to exploit this freedom for simplifying formulae
considerably. Examples for cases where this occurs
systematically are the relational translation from modal
logics to predicate logic and the relativization of
first-order logic with sorts.