IJCAR: International Joint Conference on Automated Reasoning Automated Reasoning 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings
This volume contains the papers presented at the 9th International Joint Conference on
Automated Reasoning, IJCAR 2018, held during July 14–17, 2018 in Oxford, UK, as
part of the Federated Logic Conference, FLoC 2018.
There were 125 abstracts submitted to IJCAR, resulting in 108 complete submissions.
Each submission was assigned to three Program Committee members and
received at least three reviews. The committee accepted 46 papers in total, 38 full
papers and eight system descriptions. In addition, the program included two invited
talks by Erika Abraham and Martin Giese, and accommodated a number of FLoC
IJCAR is the premier international joint conference on all aspects of automated
reasoning, including foundations, implementations, and applications, comprising several
leading conferences and workshops. It was first held in Sienna, Italy, in 2001,
uniting CADE, the Conference on Automated Deduction, TABLEAUX, the International
Conference on Automated Reasoning with Analytic Tableaux and Related
Methods, and FTP, the Workshop on First-Order Theorem Proving. Since 2004, IJCAR
has been held every second year, alternating with separate meetings of its constituent
conferences. In 2018, IJCAR united CADE, TABLEAUX, and FroCoS, the International
Symposium on Frontiers of Combining Systems, and, for the fourth time, was
part of the Federated Logic Conference. IJCAR also hosted the CADE ATP System
Competition and 11 workshops.
IJCAR acknowledges the generous sponsorship of EurAI, the European Association
for Artificial Intelligence (https://www.eurai.org/), for supporting in part our invited
We would like to thank the organizers of IJCAR, FLoC, and associated events, but
in particular the members of the IJCAR Program Committee (PC) and the additional
external reviewers. They provided high-quality reviews.
The PC chairs also would like to acknowledge EasyChair. The system was extremely
supportive for most major tasks, including the reviewing and selection of papers,
the organization of the program, and creating this proceedings volume.
May 2018 Didier Galmiche
Logical frameworks allow the specification of deductive systems using the same logical machinery. Linear logical frameworks have been successfully used for the specification of a number of computational, logics and proof systems. Its success relies on the fact that formulas can be distinguished as linear, which behave intuitively as resources, and unbounded, which behave intuitionistically. Commutative subexponentials enhance the expressiveness of linear logic frameworks by allowing the distinction of multiple contexts. These contexts may behave as multisets of formulas or sets of formulas. Motivated by applications in distributed systems and in type-logical grammar, we propose a linear logical framework containing both commutative and non-commutative subexponentials. Non-commutative subexponentials can be used to specify contexts which behave as lists, not multisets, of formulas. In addition, motivated by our applications in type-logical grammar, where the weakenening rule is disallowed, we investigate the proof theory of formulas that can only contract, but not weaken. In fact, our contraction is non-local. We demonstrate that under some conditions such formulas may be treated as unbounded formulas, which behave intuitionistically.