IJCAR 2018

IJCAR 2018
9th International Joint Conference on Automated Reasoning
Part of
FLoC 2018
July
14-17
, 2018, Oxford, UK
Conference
Call For Papers
Submission
Important Dates
Invited Speakers
Program
Proceedings
JAR Special Issue
Registration
Organization
Associated Events
FLoC 2018
IJCAR
Association for Automated Reasoning
Impressum
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
. 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
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
Erika
Ábrahám
Symbolic Computation Techniques in SMT
Solving: Mathematical Beauty meets Efficient
Heuristics
Martin
Giese
Industrial Data Access – What are the
Reasoning Problems? And is Reasoning the
Problem?
Accepted Papers
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes and Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic
Alexander Steen and Christoph Benzmüller:
The Higher-Order Prover Leo-III
Alexey Ignatiev, Filipe Pereira, Nina Narodytska and Joao Marques-Silva:
A SAT-Based Approach to Learn Explainable Decision Sets
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli and Clark Barrett:
Datatypes with Shared Selectors
André Platzer:
Uniform Substitution for Differential Game Logic
Anupam Das:
Focussing, MALL and the polynomial hierarchy
Bartosz Piotrowski and Josef Urban:
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Benjamin Kiesl, Adrian Rebola-Pardo and Marijn Heule:
Extended Resolution Simulates DRAT
Bohua Zhan and Maximilian P. L. Haslbeck:
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Cláudia Nalon and Dirk Pattinson:
A Resolution-Based Calculus for Preferential Logics
Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma:
A New Probabilistic Algorithm for Approximate Model Counting
Dennis Müller, Florian Rabe and Michael Kohlhase:
Theories as Types
Dominique Larchey-Wendling:
Constructive Decision via Redundancy-free Proof-Search
Etienne Payet and Fausto Spoto:
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov:
A FOOLish Encoding of the Next State Relations of Imperative Programs
Florian Lonsing and Uwe Egly:
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Franziska Rapp and Aart Middeldorp:
FORT 2.0
Guillaume Melquiond and Raphaël Rieu-Helft:
A Why3 framework for reflection proofs and its application to GMP's algorithms
Jacopo Urbani, Markus Krötzsch, Ceriel Jacobs, Irina Dragoste and David Carral:
Efficient Model Construction for Horn Logic with VLog: System Description
Jasmin Christian Blanchette, Nicolas Peltier and Simon Robillard:
Superposition with Datatypes and Codatatypes
Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail:
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Jens Katelaan, Dejan Jovanović and Georg Weissenbacher:
A Separation Logic with Data: Small Models and Automation
Jeremy Dawson, Nachum Dershowitz and Rajeev Gore:
Well-Founded Unions
Jochen Hoenicke and Tanja Schindler:
Efficient Interpolation for the Theory of Arrays
Julio Cesar Lopez Hernandez and Konstantin Korovin:
An abstraction-refinement framework for reasoning with large theories
Katalin Fazekas, Fahiem Bacchus and Armin Biere:
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Manuel Bodirsky and Johannes Greiner:
Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Marcelo Finger and Sandro Preto:
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
Martin Bromberger:
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Matteo Acclavio and Lutz Strassburger:
From Syntactic Proofs to Combinatorial Proofs
Max Kanovich, Stepan Kuznetsov, Vivek Nigam and Andre Scedrov:
A Logical Framework with Commutative and Non-Commutative Subexponentials
Michael Peter Lettmann and Nicolas Peltier:
A Tableaux Calculus for Reducing Proof Size
Miika Hannula and Sebastian Link:
Automated Reasoning about Key Sets
Mnacho Echenim, Nicolas Peltier and Yanis Sellami:
A Generic Framework for Implicate Generation Modulo Theories
Nao Hirokawa, Julian Nagele and Aart Middeldorp:
Cops and CoCoWeb: Infrastructure for Confluence Tools
Nicholas Smallbone and Koen Claessen:
Efficient encodings of first-order Horn formulas in equational logic
Nicolas Jeannerod and Ralf Treinen:
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
Pei Huang, Feifei Ma, Jian Zhang, Cunjing Ge and Hantao Zhang:
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Rümmer:
Exploring Approximations for Floating-Point Arithmetic using UppSAT
Sarah Winkler and Georg Moser:
MaedMax: A Maximal Ordered Completion Tool
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
Stefan Ciobaca and Dorel Lucanu:
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems
Sylvain Conchon, David Declerck and Fatiha Zaidi:
Cubicle-W: Parameterized Model Checking on Weak Memory
Yevgeny Kazakov and Peter Skočovský:
Enumerating Justifications using Resolution
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
16th International Workshop on Termination (WST 2018)
Vampire 2018: The 5th Vampire Workshop
SC2: International Workshop on Satisfiability Checking and Symbolic Computation
PRUV'18: Logics for Reasoning about Preferences, Uncertainty, and Vagueness
Theorem Prover Components for Educational Software (ThEdu'18)
Satisfiability Modulo Theories (SMT'18) Workshop
External and Internal Calculi for Non-classical Logics
Third International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018)
Practical Aspects of Automated Reasoning (PAAR-2018)
Deduction Mentoring Workshop
User Interfaces for Theorem Provers (UITP’18)
CADE ATP System Competition
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
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-Stokkermans
University 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
Image
credit:
User:
Diliff
via the
Wikimedia Commons