Towards a Workbench for Interactive Formal Reasoning
Peter Padawitz · 2005
Expander2 is a flexible multi-purpose workbench for inter- active rewriting, verification, constraint solving, flow graph analysis and other procedures that build up proofs or computation sequences. More- over, tailor-made interpreters display terms as two-dimensional struc- tures ranging from trees and rooted graphs to a variety of pictorial rep- resentations that include tables, matrices, alignments, piles, partitions, fractals and turtle systems. Proofs and computations performed with Expander2 follow the rules and the semantics of swinging types. Swinging types are based on many- sorted predicate logic and combine visible constructor-based types with hidden state-based types. The former come as initial term models, the lat- ter as final models consisting of context interpretations. Relation symbols are interpreted as least or greatest solutions of their respective axioms. This paper presents an overview of Expander2 with particular emphasis on the system's prover capabilities.