Computer Laboratory

Matej Urbas

Matej Urbas

I am a PhD student working under the supervision of Mateja Jamnik. I am interested in formal heterogeneous reasoning within general purpose proof assistants (such as Isabelle).

Heterogeneous reasoning refers to the use of diagrammatic languages and diagrammatic inference rules mixed with traditional sentential logics.

Currently, I am developing a framework, called Diabelli, which provides the infrastructure for heterogeneous reasoning. Diagrammatic and sentential reasoners can be easily integrated through Diabelli to create an interactive heterogeneous reasoning system.

Apart from the Diabelli framework I also work on a prototype instantiation of it. I am currently integrating Speedith (our diagrammatic reasoner for spider diagrams) and Isabelle. The resulting system is called Speedabelle and supports reasoning with both Isabelle/HOL formulae and spider diagrams.

Contact Information

Telephone: +44 (0) 1223 763 533
Address: Computer Laboratory
15 JJ Thomson Avenue
Cambridge, CB3 0FD
Room: FE22
PGP-key: C4DD8062 (CD93 69DC A351 05D3 BDAD 5E2B A61E F90C C4DD 8062)