An Expander2 specification consists of a signature with functions, predicates, axioms, theorems and conjectures (terms to be rewritten or formulas to be solved or proved). It describes a set of algebraic (constructor-based) and/or coalgebraic (destructor-based) types (formerly called swinging types). Syntactically, it follows Haskell (for presenting functions) and usual mathematical notations (for presenting relations and propositional, predicate-logic, modal or temporal operators). Predicates are interpreted as the least or greatest solutions of their Horn resp. co-Horn axioms.
The user interacts with the system at three levels of control over proofs and computations. At the top level, rules like Noetherian induction and incremental fixpoint co/induction are applied locally and step by step. At the medium level, goals are co/resolved or narrowed, i.e., axioms are applied exhaustively and iteratively. At the bottom level, built-in rules (some of them executing Haskell programs) simplify, i.e., (partially) evaluate terms and formulas, and thus hide routine steps of a proof or computation. Simplifications may be executed automatically after each step performed at the top or medium level.
As the co/Horn axioms co/resolved or narrowed upon are part of the user-defined specification, so additional simplification rules (equations or equivalences) may be entered into the specification. Recently, functional and logical fixpoint operators have been integrated into the simplifier along with corresponding (non-incremental) co/induction rules. Proofs and other rewrite sequences are automatically translated into proof terms that can be evaluated and modified later. Of course, a textual record listing all elements of the sequence and the rules producing them is also generated.
Expander2 has been written in O'Haskell, an extension of Haskell with object-oriented features for reactive programming and with an easy-to-use interface to Tcl/Tk. O'Haskell did not only allow us to develop a comfortable GUI for Expander2, but also to meet the other design goals of the system like the integration of testing, proving and visualizing deductive methods, working at several levels of interaction (see above) and keeping it open for extensions and adaptations of individual components to changing demands.
The prover features of Expander2 are described in more detail in P. Padawitz, Expander2 as a Prover and Rewriter (slides). This is an actualized version of P. Padawitz, Expander2: Towards a Workbench for Interactive Formal Reasoning, in: H.-J. Kreowski et al., Formal Methods in Software and Systems Modeling: Essays Dedicated to Hartmut Ehrig, Springer LNCS 3393 (2005) 236-258, and P. Padawitz, Expander2: Program verification between interaction and automation, in: F.J. Lopez Fraguas, ed., Proc. 15th Workshop on Functional and (Constraint) Logic Programming, Elsevier ENTCS 177 (2007) 35-57.
Many sample specifications, in particular of Kripke structures and coalgebraic types, along with proofs and term rewrite sequences that use them can be found here (short paper).
Overviews are also given by From fixpoint to predicate co/induction and its use in standard models (slides) and Expander2, a Haskell-based prover and rewriter (slides).
Slides on the features of Expander2 dealing with the structured generation, modification and animation of vector graphics can be found here.
Old manual: html, pdf 1, pdf 2 - New manual (in preparation): pdf - Quick Start: pdf
Send comments, bugs, etc. to Peter Padawitz. Any suggestions for improvements, extensions, applications or project proposals are welcome!
