Preface: Special Issue of Selected Extended Papers from IJCAR 2018

This special issue of the Journal of Automated Reasoning is dedicated to selected papers presented at the 9th Joint Conference on Automated Reasoning (IJCAR 2018), held between July 14 and July 17, 2018 in Oxford, UK, as part of the Federated Logic Conference (FLOC) 2018. IJCAR is the premier international joint conference on all topics in automated reasoning and merges three leading events in automated reasoning: CADE (Conference on Automated Deduction), FroCoS (Symposium on Frontiers of Combining Systems), and TABLEAUX (Conference on Analytic Tableaux and Related Methods).

The papers selected for this special issue underwent a two-round reviewing process. In the first round, the papers had been reviewed and accepted by at least three reviewers as part of the IJCAR 2018 reviewing process. We invited authors of top rated papers in the proceedings as evaluated by the reviewers to submit revised and extended versions of their papers to this special issue. In the second round, the submitted extended papers went through the reviewing process of the Journal of Automated Reasoning. Each paper was reviewed by two reviewers. The seven selected papers in this special issue cover a wide spectrum of topics in Automated Reasoning, from proof theory and theorem proving to formalization and mechanization of completeness or decidability results, from proof systems to analysis of complexity and decidability, from automated reasoning to the production of stateful ML programs together with proofs of correctness, from extensions of model checking techniques to the verification of some parameterized systems.

The paper “Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover” presents a formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving in Isabelle/HOL, providing a refutationally complete first-order prover based on ordered resolution with literal selection. It proposes general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition.

The paper “Constructive Decision via Redundancy-free Proof-Search” presents a constructive account of Kripke-Curry’s method used to establish the decidability of Implicational Relevance Logic (\(R_{\rightarrow }\)). The method is mechanized in axiom-free Coq, with the replacement of Kripke/Dickson’s lemma by a constructive form of Ramsey’s theorem and of König’s lemma by an inductive form of Brouwer’s Fan theorem. The abstract proof is instantiated to get a constructive decision procedure for \(R_{\rightarrow }\).

The paper “From QBFs to MALL and back via focussing: Fragments of multiplicative additive linear logic for each level of the polynomial hierarchy” investigates how to extract alternating time bounds from ‘focussed’ proof systems, with a refinement of focussing to consider deterministic computations in proof search. It provides fragments of Multiplicative Additive Linear Logic (MALL) with weakening, that are complete for each level of the polynomial hierarchy. This refines the well-known results that both MALL and MALL with weakening are PSPACE-complete.

The paper “Simulating Strong Practical Proof Systems with Extended Resolution” focuses on two proof systems: DRAT, used in SAT solving, and DPR that is a generalization of DRAT that allows for short proofs without the need of new variables. The paper shows that, from the viewpoint of proof complexity, these two systems are no stronger than extended resolution. It shows first that extended resolution polynomially simulates DRAT and secondly that DRAT polynomially simulates DPR. The simulations have been implemented and evaluated.

The paper “Probably Partially True Satisfiability for Lukasiewicz Infinitely-valued Probabilistic Logic and Related Topics” considers probabilistic-logic reasoning in a context that allows for “partial truths”, with a focus on computational and algorithmic properties of non-classical Lukasiewicz Infinitely-valued Probabilistic Logic. It studies the satisfiability of joint probabilistic assignments, which are called LIPSAT. This work provides linear algebraic methods that guarantee polynomial size witnesses, placing LIPSAT complexity in the NP-complete class. An exact satisfiability decision algorithm is also presented.

The paper “Proof-Producing Synthesis of CakeML from Monadic HOL Functions” provides an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. It has been developed in the HOL4 theorem prover. The proposed mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. This approach is applied to several non-trivial examples.

The paper “Parameterized Model Checking on the TSO Weak Memory Model” presents an extended version of the Model Checking Modulo Theories (MCMT) framework for verifying parameterized systems under the total store ordering (TSO) weak memory model. It proposes an axiomatic theory of this memory model based on relations over (read, write) events, a model-specific backward reachability algorithm and an SMT solver for reasoning about the formulas in this model. This framework has been implemented in the model checker Cubicle-W.

We thank the authors for their very valuable contributions, and we are especially grateful to the reviewers for their thorough and extensive feedback. We also thank Tobias Nipkow, the Editor-In-Chief of the Journal of Automated Reasoning, for his help and support for this special issue.