Expander2

[Prof. Dr. Peter Padawitz]

Expander2: A Formal Methods Presenter and Animator
==================================================

Expander2 has been designed as a multi-purpose workbench for interactive
logical inference, constraint solving, data flow analysis and other
procedures building up proofs or computation sequences. Moreover,
several interpreters translate expressions into tailor-made
two-dimensional representations that range from trees and term graphs to
tables, fractals or other turtle-system-generated pictures.

Expander2 has been implemented in O'Haskell}, an extension of
Haskell with object-oriented features for reactive programming and a
typed interface to Tcl/Tk for developing GUIs. Besides a comfortable GUI
the design goals of Expander2 were to integrate testing, proving and
visualizing deductive methods, to admit several degrees of interaction
and to keep the system open for extensions or adaptations of individual
components to changing demands.

Proofs and computations performed with Expander2 follow the rules and
the semantics of swinging types
(ls5-www.cs.uni-dortmund.de/~peter/Swinging.html). Swinging types
combine constructor-based visible types with state-based hidden types
and have unique (Herbrand) models, which interpret relations as the
least or greatest solutions of their axioms.

All features of the system and their use are described in the manual

ls5-www.cs.uni-dortmund.de/~peter/Expander2/Expander2.html 

(sorry, this is still a big file, it will be splitted soon; PostScript
version: ../Expander2/Expander2.ps.gz). The paper
..Expander2/Chiemsee.ps.gz concentrates on the prover features. Download
everything with ..Expander2.tar.gz.

Please email comments, bugs, etc. to peter.padawitz@udo.edu.

	Peter