| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Christoph Lüth, Burkhart Wolff |
| Herausgeber: |
John Harrison, Mark Aagaard |
| Titel: |
TAS —- A Generic Window Inference System |
| Buch / Sammlungs-Titel: |
Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 |
| Seite(n): |
405 – 422 |
| Serie / Reihe: |
Lecture Notes in Computer Science |
| Ausgabe: |
1869 |
| Erscheinungsjahr: |
2000 |
| Verleger: |
Springer Verlag |
| Abstract / Kurzbeschreibung: |
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. |
| PDF Version: |
http://www.informatik.uni-bremen.de/~cxl/papers/tphols00.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~cxl/papers/tphols00.ps.gz |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
03. 09. 2008 |
