Steering Committee Elections

Candidates

  • Agata Ciabattoni (Technical University Vienna)
    nominated by Christian Fermüller and Nicola Olivetti
  • Jens Otten (University of Oslo)
    nominated by Christoph Benzmüller and Renate Schmidt
  • Andrei Popescu (Middlesex University London)
    nominated by Jasmin Blanchette and Hans de Nivelle
  • Philipp Rümmer (Uppsala University)
    nominated by Reiner Hähnle and Neil Murray

Statement by Agata Ciabattoni

I am a professor at the Computer Science Faculty of the Vienna University of Technology. I am interested in non-classical logics: especially their proof theory, semantics and applications in various fields (algebra, computer science, philosophy, ..).

I feel full member of the Tableaux community: I have been regularly attending the conference and publishing there since 1999, served as PC members various time and belonging to the Tableaux Steering Committee since 2013. I am once again honored to be nominated to serve on the TSC.

I am strong in favour of having a Best Paper Award and to join Tableaux and IJCAR every second year; this schedule allows Tableaux to maintain its identity and also to enlarge the community and facilitate the exchange of ideas and techniques.

Statement by Jens Otten

TABLEAUX is the major forum for presenting work on automated reasoning with tableaux and related methods. Its main goal is to promote the development of calculi for classical and non-classical logics, their implementation and application within various disciplines. This goal can be achieved best if TABLEAUX takes place as an independent conference every two years. Co-locating with conferences such as FroCoS and ITP has been very successful in the past and should be continued in the future. In order to facilitate the exchange of ideas, TABLEAUX should continue to be part of IJCAR every other year.

My own research is focused on connection- and tableau-based automated theorem proving. I have been developing and implementing sequent, tableau and connection calculi for classical and several non-classical logics, such as intuitionistic, modal, linear, and description logic. I have developed leanCoP, a compact connection prover that has been successfully participating in the CASC ATP competition for many years. Recently, I have developed nanoCoP, a non-clausal connection prover that combines the advantages of more natural non-clausal standard tableau and sequent provers with the efficiency of a connection-based proof search. Non-classical versions of these prover belong to the fastest systems for first-order intuitionistic and several modal logics. I have initiated the development of the ILTP/QMLTP problem libraries for intuitionistic and modal logics. Since 1995 I have been attending and presenting papers at most TABLEAUX (and IJCAR) conferences.

TABLEAUX has always been open to a broad range of different calculi and logics, a tradition that should be continued in the future. At the same time TABLEAUX should try to attract more papers that describe techniques and practical experiences that lead to more efficient implementations. This could be stimulated by, for example, having a system competition for some popular non-classical logics.

Statement by Andrei Popescu

I thank the people who have nominated me and would be most honoured to serve in the steering committee.

I have participated at the previous three editions of TABLEAUX: 2013, 2014 (as part of IJCAR) and 2015. At the 2015 edition, I had the pleasure of giving a tutorial on (co)datatypes. One of my main projects, the confidentiality-verified conference management system CoCon, was used to host the TABLEAUX 2015 submission and reviewing process.

My research covers topics such as fuzzy logic, abstract model theory, universal (co)algebra, type systems, proof assistant technology (especially Isabelle) and security verification. While I am not the typical TABLEAUX researcher, I do develop, formalize, and use tableau-style proof systems on a regular basis -- for studying the Isabelle foundations, for formally verifying Isabelle's Sledgehammer tool, for developing abstract completeness results, and more.

TABLEAUX has already come a long way in establishing itself as a major event, with a clearly delimited territory in proof theory, automated deduction and both classical and non-classical logics. It has also reached a sweet spot between accessibility and high academic standards. The scientific community is now recognizing its respectable status and its strategic position. According to the widely used CORE system, TABLEAUX is ranked "A" ("excellent conference"), just like CADE. It is only together, in the IJCAR triple, that they are ranked "A*" ("flagship conference").

I would like to become involved in the process of managing TABLEAUX. If given the opportunity, I will focus on enhancing the impact of the conference. I will advocate a pragmatic approach, encouraging dialogue with applied research and with industry. Specifically:

  • We should work to ensure that the TABLEAUX results are made available to a wider community and in industry. TABLEAUX's expertise includes designing and animating proof systems for various tasks -- the software engineering community has increasing demand here (in the context of achieving reliable systems), but lacks the skills and the methodology.
  • I will advocate a more systematic approach to advertising TABLEAUX (and its high ranking) to potential authors.
  • I will seek a more active and less ad hoc policy for sponsorship. There is a growing number of verification-friendly companies that could act as long-term sponsors for a conference that promotes methods used in formal verification.
  • While continuing the successful IJCAR partnership, I would advocate co-location for odd years with major conferences having the potential of a fruitful interaction with the TABLEAUX topics, such as CAV and ITP.
  • A best-paper award and an associated journal special issue are low-hanging fruits for making the conference more attractive to authors -- I will argue for including these as permanent TABLEAUX policies. They represent win-win situations for authors, organizers and editors. There is a growing trend in computer science towards journal publications, possibly because these carry more weight in many countries. I believe TABLEAUX should embrace this trend via associations with, e.g., Theoretical Computer Science, Journal of Automated Reasoning, Studia Logica, or Logical Methods in Computer Science.

Statement by Philipp Rümmer

I am researcher at the IT Department of Uppsala University, Sweden.

Although my involvement with TABLEAUX as a conference has only been fairly recent, tableau-style calculi have been a central topic in my research ever since my PhD studies: among others because my research started at a department with long tableau traditions, and because I had the pleasure to be supervised by a number of active tableau researchers. Over the years, I have worked on and with various systems implementing tableaux, including the Java verification system KeY, and later my own theorem prover Princess, and her younger sister ePrincess (mainly developed by my PhD student Peter Backeman). One of the main themes in my work is the integration of theory reasoning in tableau systems; besides first-order theorem proving, I am also active in the area of SMT, and elected member of the Steering Committee of the SMT Workshop. I am honoured to be nominated for the TABLEAUX Steering Committee.

In my experience, TABLEAUX is a healthy and friendly community, with good diversity of topics and excellent scientific standard. Preserving this diversity is important. At the same time, I believe it is important also to keep "mainstream" developments in automated reasoning in mind; the classical automated reasoning field is moving quite rapidly, for instance since first-order theorem proving and SMT are moving closer together (or even converging), and combination of techniques from the different areas has led to rather intriguing results. For TABLEAUX to stay relevant in the long run, it is crucial to be open to such trends, and to stay well connected with other schools in automated reasoning. Alternation between IJCAR and TABLEAUX is helpful for this, and should be continued. I also found co-location with FroCoS to be fruitful. Finally, like for any community, it is crucial to attract young researchers, and set up the TABLEAUX meetings to be as supportive as possible.