Methods for Formal Analysis


methods for:
  • establishing foundations
  • evolving superstructure
  • applied abstract modelling
  • analysis of arguments
general principles: purpose is to assist decision making using abstract models
defining foundations comes first, logical foundations and kernel software capabilities
building super-structure gives a rich context (concepts, theorems, techniques) for analysis
abstract modelling of a problem space permits inference to correct solutions
deductive inference: a completely general method for the analysis and validation of deductive arguments using abstract models is presented

General Principles:

  • purpose is to assist decision making using abstract models

planning: in order to plan ahead we need to be able to predict in advance the effects of our actions
models: abstract models may be used to achieve this, permitting deduction of the effects of a plan or design in advance of implementation
deduction suffices, once abstract models are available, to establish the behaviour of the systems modelled, and can be effected by computer software
analyticity delineates the scope of what can be established by deductive methods, and hence the scope of formal analysis
precision: the key to successful modelling is the use of languages with precise meaning, which can best be established with the help of formal techniques


  • one-off application of methods for establishing foundations
  • methods for continuous development of superstructure
  • application methods build on superstructure
  • complementary modelling and analytic perspectives
foundations: one-off methods establish logical foundations and implement a logical software kernel, which must be in place before applications can begin
superstructure: methods are needed for continuous development of libraries of concept definitions, theorems, theorem proving & computational methods
applications: methods for applications use deductive methods with abstract models, and abtract models in the analysis of deductive arguments; applications are continuous with superstructure

Defining Foundations:

3-level metacyclic + informal definition
  1. cumulative hierarchy of sets
  2. polymorphic HO Set Theory
  3. large logical kernel
Sets: the cumulative hierarchy of well-founded sets will be described informally and defined formally using the language of the logical kernel
HOST: a polymorphic Higher Order Set Theory will be defined as an abstract logical system using the language of the logical kernel, with copious informal annotation to reduce ambiguity arising from meta-circularity
the logical kernel, an LCF-like system obtainable by conservative extension of HOST (including an embedding of a functional programming language) together with efficient implementation of powerful derived rules (including evaluation of functions defined in the embedded programming language)

Building Superstructure:

provides a rich context (concepts, theorems, techniques) for analysis
purpose: the superstructure provides a library of new kinds of materials for building models; these are developed in abstraction from particular applications in order to maximise re-usability of the materials and associated methods
modules: generalise mathematical theories and subroutine/object libraries, providing new kinds of entities together with operations or methods which perform computations, transformations, inference and problem solving with these new entities
automation: the emphasis is on logically sound automation, providing efficient brute computation, symbolic transformation, automatic inference, and intelligent problem solving in a modular integrated environment

Abstract Modelling:

  • of a problem space permits inference to correct solutions
mathematical modelling
may be distinguished by its emphasis on composition of behaviours of components to yield behaviours of systems; this is analogous to well constructed semantics for programming languages contrasted with messy operational definitions
automation if the semantics of a modelling language are well defined then the environment may be able to infer behaviour from model description, or infer model description from required behaviour

Deductive Inference:

  • a completely general method for the analysis and validation of deductive arguments using abstract models is presented
pre-conditions for deduction:
are not widely understood; deduction cannot begin in a vacuum
axiomatic startup in principle one could begin from a set of axioms as an agreed starting point, but how would one secure agreement on the axioms?
model as subject in practice it is best to agree the subject matter in the form of a mathematical model, before inference begins; models are a pre-requisite for sound deduction

© RBJ created 1997/12/30 modified 1997/12/31