address:  Informatik 1, Technische Universität Dortmund 

D44227 Dortmund, Germany 
phone:  +49 231 755 5108 
secretary:  +49 231 755 6223 
fax:  +49 231 755 6555 
peter.padawitz@udo.edu 
Expander2 is equipped with a GUI that permits the user to interact with the system at three levels of decreasing control over proofs and computations. At the first level, rules like induction and coinduction are applied locally and step by step. At the second level, goals are rewritten or narrowed, i.e. axioms are applied exhaustively and iteratively. At the third level, builtin rules (some of them execute Haskell programs) simplify, i.e. (partially) evaluate terms and formulas, and thus hide routine steps of a proof or computation.
Expander2 has been written in O'Haskell, an extension of Haskell with objectoriented features for reactive programming and a typed interface to Tcl/Tk. Besides a comfortable GUI the design goals of Expander2 were to integrate testing, proving and visualizing deductive methods, admit several degrees of interaction and 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. Swinging types combine constructorbased visible types with statebased hidden ones and have unique Herbrand models that interpret relations as the least or greatest solutions of their axioms.
Expander is a proof and test environment for algebraic data type specifications and functionallogic programs. Program design, test and verification are supported by tailormade deduction rules for proving Gentzen clauses, which are the most frequently used formulas for expressing requirements and queries to data types. Inductive proofs are built up from simplification, subsumption, resolution, rewriting and narrowing steps in a natural way that permits interaction on various levels. The core system is written in Standard ML. User interfaces are available for NeXTSTEP and X.
We present a number of new results on inductive theorem proving for design specifications based on Horn logic with equality. Induction is explicit here because induction orderings are supposed to be part of the specification. We show how the automatic support for program verification is enhanced if the specification satisfies a bunch of rewrite properties, summarized under the notion of canonicity. The enhancement is due to inference rules and corresponding strategies whose soundness is implied by the specification's canonicity. The second main result of the paper provides a method for proving canonicity by using the same rules, which are applied in proofs of conjectures about the specification and the functionallogic programs it contains.
Logical specifications provide an abstract level of programming where programs are given as axioms defining functions and predicates on constructorbased data types. Axiomatic function definitions are transformed into functional programs, predicate definitions are compiled into logic programs. If functions are to be implemented as logic programs, they must be flattened into predicates. In this paper, we exemplify the inverse translation: predicates used as multivalued, nondeterministic, functions are compiled into streamgenerating functions, which enumerate multiple values. Generateandtest algorithms, usually implemented as logic programs, can be realized in this way as functional programs. Our case study deals with a configuration problem. Two nondeterministic algorithms that compute rectangular dissections are specified in the functionallogic language of Expander, flattened into Prolog programs, and, alternatively, translated into ML programs, which produce streams of dissections. Besides the compilation of predicates into stream functions the case study illustrates the use of polymorphic types and higherorder functions for accomplishing wellstructured and reusable software.
Unchecked version! Chapter 12 of Einführung ins funktionale Programmieren contains a revised version.
We present a generic functional program for loading (twodimensional) containers with arbitrary objects, filling shelves with items of different kinds and  last not least  designing complete shelf systems. This piece of software and its development is a case study in functional programming for solving hierarchical configuration problems. Such problems require tailormade, but nevertheless abstract and generic data models and algorithms. We claim that these are more directly realizable in a functional language than in a classical imperative language. Polymorphism, module abstraction, semantically wellfounded exception handling and the problemoriented option for static data, "lazy" structures (streams) or dynamic objects are the main concepts of functional programming we are going to use and explain in the context of our case study.