A Framework for Formal Analysis

Introduction:

  • A framework for formal analysis and abstract modelling.
  • Languages, methods, tools.
  • Solid logical foundations; carefully articulated philosophical rationale.
Methods
supporting reliable deductive reasoning with abstract models in all application domains
Philosophy underpinning and delineating the scope of applicability of the methods
Languages providing precision notations, both general and domain specific
Logic modern classical logical foundations deliver the full power of applicable mathematics
Software provides effective support for formal analysis and modelling

Methods:

methods for:
  • establishing foundations
  • evolving superstructure
  • applied abstract modelling
  • analysis of arguments
principles: purpose is to assist decision making using abstract models
foundations must first be established, logical foundations and kernel software capabilities
superstructure provides 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

Philosophy:

  • Epistemology, phil. logic, mathematics and engineering underpin the framework.
  • Varieties of philosophical analysis are considered, a new one is presented.
History: varieties of 20thC philosophical analysis are contrasted with the formal analysis advocated here
Epistemology: familiar fundamental epistemological distinctions are identified on which formal analysis is predicated
Logic: an analysis of the nature of logical truth leads to firm logical foundations for formal analysis
Mathematics: the logicist thesis is re-affirmed and related to other positions in mathematical philosophy
Engineering: a formal analytic position is elaborated on the application of logic through mathematics in science and engineering
Philosophy: applications of formal analysis in philosophy are considered

Logic:

Single powerful classical logical foundation system provides a touchstone for analytic truth.

Feature Pedigree Rationale
modern predicate calculus Frege expressive for mathematics
the iterative conception of set. Cantor clean semantic bedrock.
logical type theory Russell consistency and discipline
axiomatic set theory with separation Zermelo consistency and flexibility
simply typed lambda-calculus Church uniform variable binding
replacement axiom for sets Fraenkel logical strength in set theory
simple polymorphism Milner more flexible type system
Gordon's polymorphic Higher Order Logic, and a classical set theory with universes and polymorphic urelements, provide a strong, conservative, pragmatic, implementable logical foundation system for formal analysis.

Languages:

  • strong core abstract foundation
  • flexible concrete representation
  • multi-lingual by semantic embedding
abstract core
powerful lightweight flexible abstract language, combining higher order logic, set theory and functional programming. Logical strength permits development by conservative extension.
flexible syntax will provide control over the concrete presentation of each new entity defined
semantic embedding will permit formal languages to be defined, syntactically and semantically, and applied using the tools
hypermedia presentation of all formal material will be supported, emerging standards (such as XML) will be intercepted
interworking will be supported by implementation of relevant standards, to be identified

Software:

  • Efficient computational problem solving in sound proof based context.
  • A fusion of proof and computation.
Logical Mega-Kernel:
software tools built around LCF-like logical kernel, with built-in compiler to give fast evaluation-in-proof.
Numeric/Symbolic/Deductive The deductive capabailities of the tools will be complemented by strength in mathematica-like symbolic and numeric capabilities.
Exact Real Analysis: real and complex analysis will be performed through the logical kernal using algorithms supporting work to arbitrary known error bounds
efficient decision procedures for arbitrary application domains can be incorporated though a "correct computation is proof" reflection principle.


UP HOME © RBJ created 1997/12/21 modified 1998/06/30