Oxford Skyline


General Information

The 9th International Joint Conference on Automated Reasoning will take place July 14-17, 2018, as part of FLoC 2018 in Oxford, United Kingdom.


IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks. IJCAR 2018 is part of the Federated Logic Conference and is the merger of leading events in automated reasoning:

  • CADE (Conference on Automated Deduction)
  • FroCoS (Symposium on Frontiers of Combining Systems)
  • TABLEAUX (Conference on Analytic Tableaux and Related Methods)

IJCAR 2018 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited.

IJCAR topics include the following ones:

  • Logics of interest include: propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, type theory, etc.
  • Methods of interest include: tableaux, sequent calculi, resolution, model-elimination, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, automated theorem provers, etc.
  • Applications of interest include: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, etc.

We welcome papers combining automated-reasoning formalisms & techniques and with those from other areas of CS and mathematics -- including, e.g., computer algebra, machine learning, formal languages, formal verification, termination. In particular, high-quality conference papers on the topics of the IJCAR 2018 affiliated workshops are welcome.

Call For Papers

The Call for Papers is available in plain (UTF-8) text format.


Please submit your papers via EasyChair at https://easychair.org/conferences/?conf=ijcar2018. The page limit for regular research papers is 16 pages. Short system descriptions should not exceed 8 pages. For more details see the Call for Papers.

Submission is closed!

Important Dates

Abstract submission deadline: January 22nd 2018
Paper submission deadline: January 29th, 2018 February 4th (9 pm AoE)
Author notification: March 29th, 2018
Camera-ready paper versions due: April 23rd, 2018
IJCAR Conference: July 14nd-17th 2018
FLoC: July 6th-19th 2018

Invited Speakers

Erika Ábrahám is Professor of Computer Science at RWTH Aachen and head of the research group Theory of Hybrid Systems. Her research areas include decision procedures, SMT-solving and bounded model checking, in particular in the context of the SC2 initiative.

Martin Giese is a Professor in the Department of Informatics at the University of Oslo, and a member of the Research Group for Logic and Intelligent Data (LOGID). His research interests include first-order logic, tableaux-based methodsy, description logics, and semantic technologies and the semantic web.

In addition, IJCAR 2018 will share two invited speakers of FLoC, Georges Gonthier and Byron Cook.

We are happy to acknowledge EurAI for their generous support of the IJCAR invited speakers.


The tabular program is now online. IJCAR will also host a number of FLoC workshops and the CADE ATP System Competition.

Invited Presentations

  1. Erika Ábrahám: Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics
  2. Martin Giese: Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem?

Accepted Papers

  1. Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes and Uwe Waldmann: Superposition for Lambda-Free Higher-Order Logic
  2. Alexander Steen and Christoph Benzmüller: The Higher-Order Prover Leo-III
  3. Alexey Ignatiev, Filipe Pereira, Nina Narodytska and Joao Marques-Silva: A SAT-Based Approach to Learn Explainable Decision Sets
  4. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann: Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
  5. Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli and Clark Barrett: Datatypes with Shared Selectors
  6. André Platzer: Uniform Substitution for Differential Game Logic
  7. Anupam Das: Focussing, MALL and the polynomial hierarchy
  8. Bartosz Piotrowski and Josef Urban: ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
  9. Benjamin Kiesl, Adrian Rebola-Pardo and Marijn Heule: Extended Resolution Simulates DRAT
  10. Bohua Zhan and Maximilian P. L. Haslbeck: Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
  11. Cláudia Nalon and Dirk Pattinson: A Resolution-Based Calculus for Preferential Logics
  12. Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma: A New Probabilistic Algorithm for Approximate Model Counting
  13. Dennis Müller, Florian Rabe and Michael Kohlhase: Theories as Types
  14. Dominique Larchey-Wendling: Constructive Decision via Redundancy-free Proof-Search
  15. Etienne Payet and Fausto Spoto: Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
  16. Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov: A FOOLish Encoding of the Next State Relations of Imperative Programs
  17. Florian Lonsing and Uwe Egly: QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
  18. Franziska Rapp and Aart Middeldorp: FORT 2.0
  19. Guillaume Melquiond and Raphaël Rieu-Helft: A Why3 framework for reflection proofs and its application to GMP's algorithms
  20. Jacopo Urbani, Markus Krötzsch, Ceriel Jacobs, Irina Dragoste and David Carral: Efficient Model Construction for Horn Logic with VLog: System Description
  21. Jasmin Christian Blanchette, Nicolas Peltier and Simon Robillard: Superposition with Datatypes and Codatatypes
  22. Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail: An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
  23. Jens Katelaan, Dejan Jovanović and Georg Weissenbacher: A Separation Logic with Data: Small Models and Automation
  24. Jeremy Dawson, Nachum Dershowitz and Rajeev Gore: Well-Founded Unions
  25. Jochen Hoenicke and Tanja Schindler: Efficient Interpolation for the Theory of Arrays
  26. Julio Cesar Lopez Hernandez and Konstantin Korovin: An abstraction-refinement framework for reasoning with large theories
  27. Katalin Fazekas, Fahiem Bacchus and Armin Biere: Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
  28. Manuel Bodirsky and Johannes Greiner: Complexity of Combinations of Qualitative Constraint Satisfaction Problems
  29. Marcelo Finger and Sandro Preto: Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
  30. Martin Bromberger: A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
  31. Matteo Acclavio and Lutz Strassburger: From Syntactic Proofs to Combinatorial Proofs
  32. Max Kanovich, Stepan Kuznetsov, Vivek Nigam and Andre Scedrov: A Logical Framework with Commutative and Non-Commutative Subexponentials
  33. Michael Peter Lettmann and Nicolas Peltier: A Tableaux Calculus for Reducing Proof Size
  34. Miika Hannula and Sebastian Link: Automated Reasoning about Key Sets
  35. Mnacho Echenim, Nicolas Peltier and Yanis Sellami: A Generic Framework for Implicate Generation Modulo Theories
  36. Nao Hirokawa, Julian Nagele and Aart Middeldorp: Cops and CoCoWeb: Infrastructure for Confluence Tools
  37. Nicholas Smallbone and Koen Claessen: Efficient encodings of first-order Horn formulas in equational logic
  38. Nicolas Jeannerod and Ralf Treinen: Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
  39. Pei Huang, Feifei Ma, Jian Zhang, Cunjing Ge and Hantao Zhang: Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
  40. Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Rümmer: Exploring Approximations for Floating-Point Arithmetic using UppSAT
  41. Sarah Winkler and Georg Moser: MaedMax: A Maximal Ordered Completion Tool
  42. Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael Norrish: Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
  43. Stefan Ciobaca and Dorel Lucanu: A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems
  44. Sylvain Conchon, David Declerck and Fatiha Zaidi: Cubicle-W: Parameterized Model Checking on Weak Memory
  45. Yevgeny Kazakov and Peter Skočovský: Enumerating Justifications using Resolution
  46. Yizheng Zhao and Renate A. Schmidt: FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics


Proceedings will be available electronically at FLoC, and are being published by Springer in the LNAI subseries of LNCS. During the conference, participants can access the Proceedings Online for free.

We also gratefully acknowledge Springer's support towards the IJCAR best paper award.

IJCAR'18 Special Issue of the Journal of Automated Reasoning

The authors of a selection of the best IJCAR'18 papers will be invited to produce an extended version of their paper for a special issue of the Journal of Automated Reasoning.


Registration to IJACR is part of the FLoC registration process.

Associated Events

IJCAR 2018 is one of the constituent meetings of FLoC 2018 and acts as the host conference for a number of affiliated events.

List of Workshops

  1. 16th International Workshop on Termination (WST 2018)
  2. Vampire 2018: The 5th Vampire Workshop
  3. SC2: International Workshop on Satisfiability Checking and Symbolic Computation
  4. PRUV'18: Logics for Reasoning about Preferences, Uncertainty, and Vagueness
  5. Theorem Prover Components for Educational Software (ThEdu'18)
  6. Satisfiability Modulo Theories (SMT'18) Workshop
  7. External and Internal Calculi for Non-classical Logics
  8. Third International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018)
  9. Practical Aspects of Automated Reasoning (PAAR-2018)
  10. Deduction Mentoring Workshop
  11. User Interfaces for Theorem Provers (UITP’18)

CADE ATP System Competition

  1. CADE ATP System Competition (CASC-J9)
    • Competition start: July 14th, 10:15
    • CASC dinner: July 15th, 18:30


Conference Chair

Program Chairs

Local Arrangements Chairs

Workshop Chair

Publicity Chair

Program committee

Carlos Areces FaMAF - Universidad Nacional de Córdoba
Alessandro Artale Free University of Bolzano-Bozen
Arnon Avron Tel-Aviv University
Franz Baader TU Dresden
Clark Barrett Stanford University
Peter Baumgartner Data 61 and CSIRO
Christoph Benzmüller Freie Universität Berlin
Armin Biere Johannes Kepler University Linz
Nikolaj Bjorner Microsoft Research
Jasmin Christian Blanchette Vrije Universiteit Amsterdam
Maria Paola Bonacina Università degli Studi di Verona
Torben Braüner Roskilde University
Agata Ciabattoni TU Wien
Leonardo de Moura Microsoft Research
Hans De Nivelle Nazarbayev University, Astana
Stéphane Demri CNRS, LSV, ENS Paris-Saclay
Clare Dixon University of Liverpool
François Fages Inria Université Paris-Saclay
Pascal Fontaine Université de Lorraine - LORIA
Didier Galmiche (Chair) Université de Lorraine - LORIA
Vijay Ganesh Waterloo
Silvio Ghilardi Università degli Studi di Milano
Jürgen Giesl RWTH Aachen
Laura Giordano DISIT Università del Piemonte Orientale
Valentin Goranko Stockholm University
Rajeev Gore The Australian National University
Alberto Griggio FBK-IRST
John Harrison Intel Corporation
Moa Johansson Chalmers Tekniska Högskola
Cezary Kaliszyk University of Innsbruck
Deepak Kapur University of New Mexico
Konstantin Korovin The University of Manchester
Laura Kovacs Vienna University of Technology
George Metcalfe University of Bern
Dale Miller INRIA and LIX/Ecole Polytechnique
Cláudia Nalon University of Brasília
Albert Oliveras Technical University of Catalonia
Nicola Olivetti LSIS Aix-Marseille University
Jens Otten University of Oslo
Lawrence Paulson University of Cambridge
Nicolas Peltier CNRS - LIG
Frank Pfenning Carnegie Mellon University
Silvio Ranise FBK-Irst
Christophe Ringeissen LORIA-INRIA
Philipp Ruemmer Uppsala University
Katsuhiko Sano Hokkaido University
Uli Sattler The University of Manchester
Renate A. Schmidt The University of Manchester
Stephan Schulz (Chair) DHBW Stuttgart
Roberto Sebastiani (Chair) University of Trento, Italy
Viorica Sofronie-StokkermansUniversity Koblenz-Landau
Thomas Sturm CNRS
Geoff Sutcliffe University of Miami
Cesare Tinelli The University of Iowa
Alwen Tiu Nanyang Technological University
Ashish Tiwari SRI International
Josef Urban Czech Technical University in Prague
Luca Viganò King's College London
Uwe Waldmann Max Planck Institute for Informatics
Christoph Weidenbach Max Planck Institute for Informatics