Automated Reasoning

Front Matter ....Pages I-XVIII
 An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem  (Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail)....Pages 1-18
 FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics  (Yizheng Zhao, Renate A. Schmidt)....Pages 19-27
 Superposition for Lambda-Free Higher-Order Logic  (Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann)....Pages 28-46
 Automated Reasoning About Key Sets  (Miika Hannula, Sebastian Link)....Pages 47-63
 A Tableaux Calculus for Reducing Proof Size  (Michael Peter Lettmann, Nicolas Peltier)....Pages 64-80
 FORT 2.0  (Franziska Rapp, Aart Middeldorp)....Pages 81-88
 Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover  (Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann)....Pages 89-107
 The Higher-Order Prover Leo-III  (Alexander Steen, Christoph Benzmüller)....Pages 108-116
 Well-Founded Unions  (Jeremy Dawson, Nachum Dershowitz, Rajeev Goré)....Pages 117-133
 Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories  (Katalin Fazekas, Fahiem Bacchus, Armin Biere)....Pages 134-151
 Cubicle-\\(\\mathcal {W}\\): Parameterized Model Checking on Weak Memory  (Sylvain Conchon, David Declerck, Fatiha Zaïdi)....Pages 152-160
 \\({\\textsf {QRAT}}^{+}\\): Generalizing QRAT by a More Powerful QBF Redundancy Property  (Florian Lonsing, Uwe Egly)....Pages 161-177
 A Why3 Framework for Reflection Proofs and Its Application to GMP’s Algorithms  (Guillaume Melquiond, Raphaël Rieu-Helft)....Pages 178-193
 Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic  (Marcelo Finger, Sandro Preto)....Pages 194-210
 Uniform Substitution for Differential Game Logic  (André Platzer)....Pages 211-227
 A Logical Framework with Commutative and Non-commutative Subexponentials  (Max Kanovich, Stepan Kuznetsov, Vivek Nigam, Andre Scedrov)....Pages 228-245
 Exploring Approximations for Floating-Point Arithmetic Using UppSAT  (Aleksandar Zeljić, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer)....Pages 246-262
 Complexity of Combinations of Qualitative Constraint Satisfaction Problems  (Manuel Bodirsky, Johannes Greiner)....Pages 263-278
 A Generic Framework for Implicate Generation Modulo Theories  (Mnacho Echenim, Nicolas Peltier, Yanis Sellami)....Pages 279-294
 A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems  (Ştefan Ciobâcă, Dorel Lucanu)....Pages 295-311
 A New Probabilistic Algorithm for Approximate Model Counting  (Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma)....Pages 312-328
 A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems  (Martin Bromberger)....Pages 329-345
 Cops and CoCoWeb: Infrastructure for Confluence Tools  (Nao Hirokawa, Julian Nagele, Aart Middeldorp)....Pages 346-353
 Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing  (Pei Huang, Feifei Ma, Cunjing Ge, Jian Zhang, Hantao Zhang)....Pages 354-369
 Superposition with Datatypes and Codatatypes  (Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard)....Pages 370-387
 Efficient Encodings of First-Order Horn Formulas in Equational Logic  (Koen Claessen, Nicholas Smallbone)....Pages 388-404
 A FOOLish Encoding of the Next State Relations of Imperative Programs  (Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov)....Pages 405-421
 Constructive Decision via Redundancy-Free Proof-Search  (Dominique Larchey-Wendling)....Pages 422-438
 Deciding the First-Order Theory of an Algebra of Feature Trees with Updates  (Nicolas Jeannerod, Ralf Treinen)....Pages 439-454
 A Separation Logic with Data: Small Models and Automation  (Jens Katelaan, Dejan Jovanović, Georg Weissenbacher)....Pages 455-471
 MædMax: A Maximal Ordered Completion Tool  (Sarah Winkler, Georg Moser)....Pages 472-480
 From Syntactic Proofs to Combinatorial Proofs  (Matteo Acclavio, Lutz Straßburger)....Pages 481-497
 A Resolution-Based Calculus for Preferential Logics  (Cláudia Nalon, Dirk Pattinson)....Pages 498-515
 Extended Resolution Simulates DRAT  (Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule)....Pages 516-531
 Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle  (Bohua Zhan, Maximilian P. L. Haslbeck)....Pages 532-548
 Efficient Interpolation for the Theory of Arrays  (Jochen Hoenicke, Tanja Schindler)....Pages 549-565
 ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback  (Bartosz Piotrowski, Josef Urban)....Pages 566-574
 Theories as Types  (Dennis Müller, Florian Rabe, Michael Kohlhase)....Pages 575-590
 Datatypes with Shared Selectors  (Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark Barrett)....Pages 591-608
 Enumerating Justifications Using Resolution  (Yevgeny Kazakov, Peter Skočovský)....Pages 609-626
 A SAT-Based Approach to Learn Explainable Decision Sets  (Alexey Ignatiev, Filipe Pereira, Nina Narodytska, Joao Marques-Silva)....Pages 627-645
 Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions  (Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish)....Pages 646-662
 An Abstraction-Refinement Framework for Reasoning with Large Theories  (Julio Cesar Lopez Hernandez, Konstantin Korovin)....Pages 663-679
 Efficient Model Construction for Horn Logic with VLog  (Jacopo Urbani, Markus Krötzsch, Ceriel Jacobs, Irina Dragoste, David Carral)....Pages 680-688
 Focussing, \\(\\mathsf {MALL}\\) and the Polynomial Hierarchy  (Anupam Das)....Pages 689-705
 Checking Array Bounds by Abstract Interpretation and Symbolic Expressions  (Étienne Payet, Fausto Spoto)....Pages 706-722
Back Matter ....Pages 723-724