[Club2] talk by Lars Hupel, Monday July 29, 14:00, room: Turing (00.09.38)

[Andrei Popescu]

Dear All, 

This Monday, Lars Hupel will give his Master's thesis presentation. 

Cheers, 
   Andrei

Lars Hupel
A Visualization Toolkit for Simplifier Traces in Isabelle/jEdit
===============================================================
Monday July 29, 14:00, room: Turing (00.09.38)

The simplifier in Isabelle is a very powerful tactic to discharge large
classes of goals automatically. However, the results of simplifying a term
not always match the user's expectation: sometimes, the resulting term is
not small enough, or the simplifier even failed to apply any rule. For
these cases, the simplifier offers a trace which precisely logs all steps
which have been made.

These traces can be huge, especially because the library of Isabelle/HOL
offers many pre-defined rewriting rules. It is often very difficult for
the user to find the necessary piece of information about why and what
exactly failed. Furthermore, there is no way to inspect or even influence
the system while the simplification is still running. Hence, a simple,
linear trace is not sufficient in these situations.

In this talk, we will present a new tracing facility which offers
interactivity and a high amount of configurability. It combines successful
approaches from other logic languages and adapts them to the Isabelle
setup. Furthermore, it fits neatly into the Isabelle/jEdit IDE. 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130726/eace6d0b/attachment.html>