VINO 2017

The first Viennese INter-reasoning wOrkshop

The workshop takes inspiration from the successful series of PIWo inter-reasoning workshops organised by the Automated Reasoning Group in Prague. In a similar spirit, it will combine high-quality invited presentations with informal discussions and a cultural networking programme.

The main topic of the workshop will be the combination of automated reasoning and machine learning.


7–9 September


Seminarraum 187/2, second floor, Favoritenstrasse 9–11, TU Wien, Vienna, Austria

Workshop program:


10:00–11:00 Christian Szegedy Applications of Deep Learning to ATP in large theories
11:00–11:30 coffee break
11:30–12:30 Josef Urban AI4REASON, a basic overview
12:30–14:30 lunch 
14:30–15:00 Jan Jakubův Automated Invention of Strategies and Term Orderings for Vampire
15:00–15:30 Michael Färber Nonclausal Proof Search for Dummies
15:30–16:00 coffee break
16:00–16:30 Julian Parsert Formalization of the First Theorem of Welfare Economics
16:30–17:00 discussion
19:00–… workshop dinner (at Waldviertlerhof)


10:00–11:00 Arnold Neumaier From Informal to Formal Mathematics
11:00–11:30 coffee break
11:30–12:30 Chad Brown and Jiří Vyskočil Recovering Formal Representations from Informalized Mizar Sentences
12:30–14:30 lunch
14:30–15:00 Benjamin Kiesl Short Proofs Without New Variables
15:00–15:30 Adrian Rebola Pardo Learning History and Eager to Repeat It
15:30–16:00   coffee break
16:00–16:30 Henryk Michalewski Xgboost-based Evaluation Function in leancop
16:30–17:00 Thibault Gauthier Abracadabra (TacticToe, a Tactic-based Prover for HOL4)
19:00–…   networking dinner (at Werner Welser Heuriger)


from 10:00; a hike in the forests of Vienna

Invited speakers:


  • Lasse Blaauwbroek, CIIRC
  • Chad Brown, CIIRC
  • Michael Färber, University of Innsbruck
  • Thibault Gauthier, University of Innsbruck
  • Zar Goertzel, CIIRC
  • Karel Chvalovský, CIIRC
  • Jan Jakubův, CIIRC
  • Benjamin Kiesl, TU Wien
  • Henryk Michalewski, University of Warsaw
  • Adrian Rebola Pardo, TU Wien
  • Julian Parsert, University of Innsbruck
  • Bartosz Piotrowski, University of Warsaw
  • Josef Urban, CIIRC
  • Jiří Vyskočil, CIIRC

Workshop organiser:


The workshop is partially supported by the ERC Starting Grant 2014 – SYMCAR 639270.

Latest News

Jens Pagel wins Bill McCune PhD Award

We congratulate Jens Pagel for receiving the 2021 Bill McCune PhD Award in Automated Reasoning! Jens graduated in 2020; his thesis on Decision procedures for separation logic: beyond symbolic heaps (supervised by Florian Zuleger) presents his substantial contributions to the theory of formal verification and automated reasoning, and to verifying heap-manipulating programs in particular.

Continue reading

Full news archive