Frontiers of Combining Systems: 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings (Lecture Notes in Computer Science Book 11715)

This book constitutes the proceedings of the 12th International Symposium on Frontiers of Combining Systems, FroCoS 2019, held in London, UK, in September 2019, colocated with the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019. The 20 papers presented were carefully reviewed and selected from 30 submissions. They present research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. The papers are organized in the following topical sections: automated theorem proving and model building, combinations of systems, constraint solving, description logics, interactive theorem proving, modal and epistemic logics, and rewriting and unification. Front Matter ....Pages i-xx Front Matter ....Pages 1-1 Symmetry Avoidance in MACE-Style Finite Model Finding (Giles Reger, Martin Riener, Martin Suda)....Pages 3-21 On the Expressivity and Applicability of Model Representation Formalisms (Andreas Teucke, Marco Voigt, Christoph Weidenbach)....Pages 22-39 A Neurally-Guided, Parallel Theorem Prover (Michael Rawson, Giles Reger)....Pages 40-56 A Language-Independent Framework for Reasoning About Preferences for Declarative Problem Solving (Alireza Ensan, Eugenia Ternovska)....Pages 57-73 Front Matter ....Pages 75-75 Ilinva: Using Abduction to Generate Loop Invariants (Mnacho Echenim, Nicolas Peltier, Yanis Sellami)....Pages 77-93 An Algebra of Modular Systems: Static and Dynamic Perspectives (Eugenia Ternovska)....Pages 94-111 Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations (David Fuenmayor, Christoph Benzmüller)....Pages 112-128 Front Matter ....Pages 129-129 A CDCL-Style Calculus for Solving Non-linear Constraints (Franz Brauße, Konstantin Korovin, Margarita Korovina, Norbert Müller)....Pages 131-148 Restricted Cutting Plane Proofs in Horn Constraint Systems (Hans Kleine Büning, Piotr Wojciechowski, R. Chandrasekaran, K. Subramani)....Pages 149-164 Front Matter ....Pages 165-165 The Complexity of the Consistency Problem in the Probabilistic Description Logic \(\mathcal {ALC} ^\mathsf {ME}\) (Franz Baader, Andreas Ecke, Gabriele Kern-Isberner, Marco Wilhelm)....Pages 167-184 Extending Forgetting-Based Abduction Using Nominals (Warren Del-Pinto, Renate A. Schmidt)....Pages 185-202 On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets (Franz Baader, Filippo De Bortoli)....Pages 203-219 Front Matter ....Pages 221-221 Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL (Ralph Bottesch, Max W. Haslbeck, René Thiemann)....Pages 223-239 Verifying Randomised Social Choice (Manuel Eberl)....Pages 240-256 Front Matter ....Pages 257-257 Epistemic Reasoning with Byzantine-Faulty Agents (Roman Kuznets, Laurent Prosperi, Ulrich Schmid, Krisztina Fruzsa)....Pages 259-276 Two Is Enough – Bisequent Calculus for S5 (Andrzej Indrzejczak)....Pages 277-294 Front Matter ....Pages 295-295 On Asymmetric Unification for the Theory of XOR with a Homomorphism (Christopher Lynch, Andrew M. Marshall, Catherine Meadows, Paliath Narendran, Veena Ravishankar)....Pages 297-312 Reviving Basic Narrowing Modulo (Dohan Kim, Christopher Lynch, Paliath Narendran)....Pages 313-329 Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems (Takahito Aoto, Yoshihito Toyama)....Pages 330-347 Transforming Derivational Complexity of Term Rewriting to Runtime Complexity (Carsten Fuhs)....Pages 348-364 Back Matter ....Pages 365-365