Preface: Special Issue of Selected Extended Papers from IJCAR 2018
- PDF / 185,451 Bytes
- 3 Pages / 439.37 x 666.142 pts Page_size
- 81 Downloads / 245 Views
Preface: Special Issue of Selected Extended Papers from IJCAR 2018 Didier Galmiche1 · Stephan Schulz2
· Roberto Sebastiani3
Received: 17 April 2020 / Accepted: 24 April 2020 © The Author(s) 2020
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→ ). 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
B
Stephan Schulz [email protected]
1
LORIA, CNRS, Université de Lorraine, Nancy, France
2
Duale Hochschule Baden-Württemberg Stuttgart, Stuttgart, Germany
3
Department of Information Engineering and Computer Science, University of Trento, Trento, Italy
123
D. Galmiche et al.
lemma by an inductive form of Brouwer’s Fan theorem. The abstract proof is instantiated to get a constructive decision procedure for R→ . The paper “From QBFs to MALL
Data Loading...
