[Club2] Thu. Sept. 8, 14:00, talk by Matej Urbas

[Andrei Popescu]

Dear All,

On Thursday, we have a talk by Matej Urbas, who's visiting Thomas this weak. Info follows.  

Cheers, 
  Andrei    

Matej Urbas
Heterogeneous reasoning with spider diagrams and Isabelle/HOL
====================================================
Thu. Sept. 8, 14:00, MI 00.09.055 ("Alan Turing")

Abstract:

    I will outline the ongoing work of integrating a diagrammatic
reasoner with Isabelle. The goal is to produce a heterogeneous reasoning
framework, which will allow the user to interactively mix diagrammatic
and sentential proof steps.

    The term `heterogeneous' refers to reasoning in two languages: One
is diagrammatic, for which we have chosen the language of spider
diagrams, and the other one is sentential, for which we use
Isabelle/HOL. The latter is also used to formalise spider diagrams,
translate between the two languages, and reconstruct diagrammatic proof
steps.

    In the end, I will briefly introduce plans and considerations for
the user interface of the framework.