Conference

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.

Scope

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.

Submission

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.

Important Dates

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 SC² 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.

Program

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

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

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

Organization

Conference Chair

• Ian Horrocks

Program Chairs

• Didier Galmiche
• Stephan Schulz
• Roberto Sebastiani

Local Arrangements Chairs

• Daniel Kroening
• Marta Kwiatkowska

Workshop Chair

• Alberto Griggio (also see the list of IJCAR-2018 workshops)

Publicity Chair

• Geoff Sutcliffe

Program committee