TAS
swMATH ID:  4900 
Software Authors:  Christoph Lüth; Burkhart Wolff 
Description:  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 commandlanguagefree user interaction by gestures like drag&drop and proofbypointing, 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. 
Homepage:  http://www.informatik.unibremen.de/~cxl/tas/ 
Dependencies:  Isabelle 
Related Software:  IsaWin; Isabelle; Nuprl; HOL; CASL; LambdaClam; TeXmacs; Proof General; Mizar; Isar; IsaPlanner; ML; TPS; Coq; Proof General Kit; Isabelle/Isar; Atelier B; ArcAngel; Isabelle/HOL; PROSPER 
Referenced in:  11 Publications 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

TAS – a generic window inference system. Zbl 0974.68507 Lüth, Christoph; Wolff, Burkhart 
2000

all
top 5
Referenced by 16 Authors
all
top 5
Referenced in 6 Serials
1  Journal of Symbolic Computation 
1  Journal of Applied NonClassical Logics 
1  Nordic Journal of Computing 
1  Journal of Functional Programming 
1  Doklady Mathematics 
1  Journal of Applied Logic 
Referenced in 3 Fields
10  Computer science (68XX) 
2  Mathematical logic and foundations (03XX) 
1  Linear and multilinear algebra; matrix theory (15XX) 