TAS -- a generic window inference system This paper presents work on technology for transformational proof and program development, as used by window inference calculi and transformation systems. The calculi are characterised by a certain class of theorems in the underlying logic. Our transformation system TAS compiles these rules to concrete deduction support, complete with a graphical user interface with command-language-free user interaction by gestures like drag&drop and proof-by-pointing, and a development management for transformational proofs. It is generic in the sense that it is completely independent of the particular window inference or transformational calculus, and can be instantiated to many different ones; three such instantiations are presented in the paper.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Aspinall, David; Lüth, Christoph; Wolff, Burkhart: Assisted proof document authoring (2006)
- Dixon, Lucas; Fleuriot, Jacques: A proof-centric approach to mathematical assistants (2006)
- Ikramov, Kh. D.: A criterion for the unitary congruence of conjugate-normal matrices (2006)
- Autexier, Serge; Mossakowski, Till: Integrating HOL-CASL into the development graph manager MAYA (2002)
- Dosch, Walter; Magnussen, Sönke: The Lübeck transformation system: A transformation system for equational higher order algebraic specifications (2001)
- Anderson, Penny; Basin, David: Program development schemata as derived rules (2000)
- Lüth, Christoph; Wolff, Burkhart: TAS -- a generic window inference system (2000)
- Lüth, C.; Wolff, B.: Functional design and implementation of graphical user interfaces for theorem provers (1999)
- Aguilera, Gabriel; de Guzmán, Inma P.; Ojeda, Manuel: Increasing the efficiency of automated theorem proving (1995)
- Aguilera, G.; de Guzmán, I. P.; Ojeda, M.: $\textTAS-D^++$: Syntactic trees transformations for automated theorem proving (1994)