Automated Reasoning: 9th International Joint Conference, Ijcar 2018, Held as Part of the Federated Logic Conference, Floc 2018, Oxford, Uk, July 14-17 (Paperback, 2018)

An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem.- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics.- Superposition for Lambda-Free Higher-Order Logic.- Automated Reasoning about Key Sets.- A Tableaux Calculus for Reducing Proof Size.- FORT 2.0.- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.- The Higher-Order Prover Leo-III.- Well-Founded Unions.- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories.- Cubicle-W: Parameterized Model Checking on Weak Memory.- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property.- A Why3 framework for reflection proofs and its application to GMP's algorithms.- Infinitely-valued Logic.- Uniform Substitution for Differential Game Logic.- A Logical Framework with Commutative and Non-Commutative Subexponentials.- Exploring Approximations for Floating-Point Arithmetic using UppSAT.- Complexity of Combinations of Qualitative Constraint Satisfaction Problems.- A Generic Framework for Implicate Generation Modulo Theories.- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems.- A New Probabilistic Algorithm for Approximate Model Counting.- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems.- Cops and CoCoWeb: Infrastructure for Conuence Tools.- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing.- Superposition with Datatypes and Codatatypes.- Efficient encodings of first-order Horn formulas in equational logic.- A FOOLish Encoding of the Next State Relations of Imperative Programs.- Constructive Decision via Redundancy-free Proof-Search.- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates.- A Separation Logic with Data: Small Models and Automation.- MaedMax: A Maximal Ordered Completion Tool.- From Syntactic Proofs to Combinatorial Proofs.- A Resolution-Based Calculus for Preferential Logics.- Extended Resolution Simulates DRAT.- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle.- Efficient Interpolation for the Theory of Arrays.- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.- Theories as Types.- Datatypes with Shared Selectors.- Enumerating Justifications using Resolution.- A SAT-Based Approach to Learn Explainable Decision Sets.- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.- An abstraction-refinement framework for reasoning with large theories.- Efficient Model Construction for Horn Logic with VLog: System Description.- Focussing, MALL and the polynomial hierarchy.- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions.