The KIV - System

The logic used is a variant of dynamic logic adapted for use within a theorem prover. This adaptation builds on oldblatt's work, on uninterpreted dynamic logic. The Omega-rules used in in order to achieve completeness, have been replaced by an approximating (object-) programming language construct which refers to an auxiliary data type of counters, and an induction principle for counters. While this yields an incomplete calculus, this formalism turned out to be powerful enough for all practical purposes. Among others, the formalism allows the derivation of Hoare's invariance rule; together with an induction principle for user-defined data structures it can be used for Burstall's intermittent assertion method. In addition it can simulate a variety of other logics. For recursive procedures with procedural parameters, an auxiliary data structure of environments has been used in a similar (albeit more complex) way. Within this general formalism, special purpose rule systems can be derived.

The meta-language of the KIV system, PPL, is a typed functional language in the style of ML. The basic data structure of PPL are proof trees. These are trees of sequents, where the root is the assertion to be proved, and the leaves are either closed (i.e. correspond to some axiom) or open. In the latter case the proof is partial. Each step in a proof tree corresponds to a rule application. There are two kinds of rules, basic rules (built in to axiomatise the object logic), and user-defined rules. The latter include either a function or another tree as validation. If the validation is a tree, then it must fit, i.e. this tree's premises must be a subset of the premises of the rule, and its conclusion must be the same. If the validation is a function, it must return a fitting tree if called with the conclusion and hypothesis of the rule. The point in time at which the validation is called can be freely chosen, and thus the validation may depend on the actual instance of the rule after all of its meta-variables (see below) have been instantiated (the instantiation may take place after the rule application itself).

Rules may be schematic, in that their sequents may contain meta-variables for all syntactical categories. When combining two proof trees with the functions refine(t_1,n,t_2), the system computes a matcher for the meta-variables in t_2 such that the instantiated conclusion will be equal to the n-th premise of t_1. If any of the operations on trees cannot be performed (e.g. if no matcher exists or a validation tree does not fit), a failure is raised that may be trapped by the backtracking constructs.

Within KIV, numerous strategies for verification e.g. Hoare's calculus and Burstall's intermittent assertion method, modification and development of programs, e.g. methods by Bergstra/Klop, Dershowitz and Smith,, and for modular systems, have been implemented and to some degree been integrated.