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