Abstract
Expander2 is a flexible multi-purpose workbench for interactive rewriting, verification, constraint solving, flow graph analysis and other procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as two-dimensional structures ranging from trees and rooted graphs to a variety of pictorial representations 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 latter 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Antoy, S., Echahed, R., Hanus, M.: A Needed Narrowing Strategy. Journal of the ACM 47, 776–822 (2000)
Automated Reasoning Systems, http://www-formal.stanford.edu/clt/ARS/systems.html
Bidoit, M., Mosses, P.D. (eds.): CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)
Frühwirth, T., Abdennadher, S.: Essentials of Constraint Programming. Springer, Heidelberg (2003)
Giegerich, R.: A Systematic Approach to Dynamic Programming in Bioinformatics. Parts 1 and 2: Sequence Comparison and RNA Folding, Report 99-05, Technical Department, University of Bielefeld (1999)
Goguen, J., Malcolm, G.: A Hidden Agenda. Theoretical Computer Science 245, 55–101 (2000)
Hanus, M. (ed.): Curry: A Truly Integrated Functional Logic Language, http://www.informatik.uni-kiel.de/~curry
Haskell: A Purely Functional Language, http://haskell.org
Jacobs, B., Rutten, J.: A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62, 222–259 (1997)
The Maude System, http://maude.cs.uiuc.edu
Mossakowski, T., Reichel, H., Roggenbach, M., Schröder, L.: Algebraiccoalgebraic specification in CoCASL. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 376–392. Springer, Heidelberg (2003)
Nordlander, J. (ed.): The O’Haskell homepage, http://www.cs.chalmers.se/~nordland/ohaskell
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Padawitz, P.: Deduction and Declarative Programming. Cambridge University Press, Cambridge (1992)
Padawitz, P.: Inductive Theorem Proving for Design Specifications. J. Symbolic Computation 21, 41–99 (1996)
Padawitz, P.: Proof in Flat Specifications. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) Algebraic Foundations of Systems Specification, IFIP Stateof- the-Art Report. Springer, Heidelberg (1999)
Padawitz, P.: Swinging Types = Functions + Relations + Transition Systems. Theoretical Computer Science 243, 93–165 (2000)
Padawitz, P.: Structured Swinging Types, http://ls5-www.cs.uni-dortmund.de/~peter/SST.ps.gz
Padawitz, P.: Dialgebraic Swinging Types, http://ls5-www.cs.uni-dortmund.de/~peter/Dialg.ps.gz
Padawitz, P.: Swinging Types At Work, http://ls5-www.cs.uni-dortmund.de/~peter/BehExa.ps.gz
Padawitz, P.: Expander2: A Formal Methods Presenter and Animator, http://ls5-www.cs.uni-dortmund.de/~peter/Expander2/Expander2.html
The QPQ Database of Deductive Software Components, http://www.qpq.org
Reichel, H.: An Approach to Object Semantics based on Terminal Coalgebras. Math. Structures in Comp. Sci. 5, 129–152 (1995)
Rozenberg, G., Salomaa, A. (eds.): Handbook of Formal Languages. Beyond Words, vol. 3. Springer, Heidelberg (1997)
Schröder, L., Mossakowski, T.: Monad-independent dynamic logic in hascasl. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 425–441. Springer, Heidelberg (2003)
Stehr, M.-O., Meseguer, J., Ölveczky, P.C.: Rewriting Logic as a Unifying Framework for Petri Nets. In: Ehrig, H., Juhás, G., Padberg, J., Rozenberg, G. (eds.) APN 2001. LNCS, vol. 2128, p. 250. Springer, Heidelberg (2001)
Sutcliffe, G.: Problem Library for Automated Theorem Proving, http://www.cs.miami.edu/~tptp
Wiedijk, F. (ed.): The Digital Math Database, http://www.cs.kun.nl/~freek/digimath
The Yahoda Verification Tools Database, http://anna.fi.muni.cz/yahoda
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Padawitz, P. (2005). Expander2. In: Kreowski, HJ., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds) Formal Methods in Software and Systems Modeling. Lecture Notes in Computer Science, vol 3393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31847-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-31847-7_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24936-8
Online ISBN: 978-3-540-31847-7
eBook Packages: Computer ScienceComputer Science (R0)