EXPANDER: Inductive Expansion in SML. EXPANDER is a proof support system for reasoning about data type specifications and declarative programs. EXPANDER applies the rules of inductive expansion (cf. Chapter 5) to correctness conditions that are given as single Gentzen clauses or sets of guarded Horn clauses (cf. Chapter 2). The system provides a kernel for special-purpose theorem provers, which are tailored to restricted application areas and implement specific proof plans, strategies or tactics. It is written in the functional language SML/NJ. EXPANDER executes single inference steps. Each proof is a sequence of goal sets. The user has full control over the proof process. He may backtrack the sequence, interactively modify the underlying specification and add lemmas or induction orderings suggested by subgoals obtained so far. When a proof has been finished, the system can generate the theorems actually proved and, if necessary, the remaining subconjectures. We first describe the kind of specifications that can be processed, then present the commands currently provided and, finally, document the implementation. The latter serves for illustrating the suitability of functional languages for encoding deductive methods.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Padawitz, Peter: Expander2: program verification between interaction and automation (2007)
- Hofbauer, Dieter: An upper bound on the derivational complexity of Knuth-Bendix orderings. (2003)
- Hofbauer, Dieter; Huber, Maria: Test sets for the universal and existential closure of regular tree languages. (2002)
- Stratulat, Sorin: A general framework to build contextual cover set induction provers (2001)
- Padawitz, P.: Swinging types=functions+relations+transition systems (2000)
- Padawitz, Peter: Deduction and declarative programming (1992)