Abstract is missing.
- An Assumption-Based Approach for Solving the Minimal S5-Satisfiability ProblemJean-Marie Lagniez, Daniel Le Berre, Tiago De Lima, Valentin Montmirail. 1-18 [doi]
- FAME: An Automated Tool for Semantic Forgetting in Expressive Description LogicsYizheng Zhao, Renate A. Schmidt. 19-27 [doi]
- Superposition for Lambda-Free Higher-Order LogicAlexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann. 28-46 [doi]
- Automated Reasoning About Key SetsMiika Hannula, Sebastian Link. 47-63 [doi]
- A Tableaux Calculus for Reducing Proof SizeMichael Peter Lettmann, Nicolas Peltier. 64-80 [doi]
- FORT 2.0Franziska Rapp, Aart Middeldorp. 81-88 [doi]
- Formalizing Bachmair and Ganzinger's Ordered Resolution ProverAnders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann. 89-107 [doi]
- The Higher-Order Prover Leo-IIIAlexander Steen, Christoph Benzmüller. 108-116 [doi]
- Well-Founded UnionsJeremy E. Dawson, Nachum Dershowitz, Rajeev Goré. 117-133 [doi]
- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo TheoriesKatalin Fazekas, Fahiem Bacchus, Armin Biere. 134-151 [doi]
- W : Parameterized Model Checking on Weak MemorySylvain Conchon, David Declerck, Fatiha Zaïdi. 152-160 [doi]
- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy PropertyFlorian Lonsing, Uwe Egly. 161-177 [doi]
- A Why3 Framework for Reflection Proofs and Its Application to GMP's AlgorithmsGuillaume Melquiond, Raphaël Rieu-Helft. 178-193 [doi]
- Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued LogicMarcelo Finger, Sandro Preto. 194-210 [doi]
- Uniform Substitution for Differential Game LogicAndré Platzer. 211-227 [doi]
- A Logical Framework with Commutative and Non-commutative SubexponentialsMax I. Kanovich, Stepan Kuznetsov, Vivek Nigam, Andre Scedrov. 228-245 [doi]
- Exploring Approximations for Floating-Point Arithmetic Using UppSATAleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer. 246-262 [doi]
- Complexity of Combinations of Qualitative Constraint Satisfaction ProblemsManuel Bodirsky, Johannes Greiner. 263-278 [doi]
- A Generic Framework for Implicate Generation Modulo TheoriesMnacho Echenim, Nicolas Peltier, Yanis Sellami. 279-294 [doi]
- A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting SystemsStefan Ciobaca, Dorel Lucanu. 295-311 [doi]
- A New Probabilistic Algorithm for Approximate Model CountingCunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma. 312-328 [doi]
- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded ProblemsMartin Bromberger. 329-345 [doi]
- Cops and CoCoWeb: Infrastructure for Confluence ToolsNao Hirokawa, Julian Nagele, Aart Middeldorp. 346-353 [doi]
- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability TestingPei Huang, Feifei Ma, Cunjing Ge, Jian Zhang, Hantao Zhang. 354-369 [doi]
- Superposition with Datatypes and CodatatypesJasmin Christian Blanchette, Nicolas Peltier, Simon Robillard. 370-387 [doi]
- Efficient Encodings of First-Order Horn Formulas in Equational LogicKoen Claessen, Nicholas Smallbone. 388-404 [doi]
- A FOOLish Encoding of the Next State Relations of Imperative ProgramsEvgenii Kotelnikov, Laura Kovács, Andrei Voronkov. 405-421 [doi]
- Constructive Decision via Redundancy-Free Proof-SearchDominique Larchey-Wendling. 422-438 [doi]
- Deciding the First-Order Theory of an Algebra of Feature Trees with UpdatesNicolas Jeannerod, Ralf Treinen. 439-454 [doi]
- A Separation Logic with Data: Small Models and AutomationJens Katelaan, Dejan Jovanovic, Georg Weissenbacher. 455-471 [doi]
- MædMax: A Maximal Ordered Completion ToolSarah Winkler, Georg Moser. 472-480 [doi]
- From Syntactic Proofs to Combinatorial ProofsMatteo Acclavio, Lutz Straßburger. 481-497 [doi]
- A Resolution-Based Calculus for Preferential LogicsCláudia Nalon, Dirk Pattinson. 498-515 [doi]
- Extended Resolution Simulates DRATBenjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule. 516-531 [doi]
- Verifying Asymptotic Time Complexity of Imperative Programs in IsabelleBohua Zhan, Maximilian P. L. Haslbeck. 532-548 [doi]
- Efficient Interpolation for the Theory of ArraysJochen Hoenicke, Tanja Schindler. 549-565 [doi]
- ATPboost: Learning Premise Selection in Binary Setting with ATP FeedbackBartosz Piotrowski, Josef Urban. 566-574 [doi]
- Theories as TypesDennis Müller, Florian Rabe, Michael Kohlhase. 575-590 [doi]
- Datatypes with Shared SelectorsAndrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark Barrett. 591-608 [doi]
- Enumerating Justifications Using ResolutionYevgeny Kazakov, Peter Skocovský. 609-626 [doi]
- A SAT-Based Approach to Learn Explainable Decision SetsAlexey Ignatiev, Filipe Pereira, Nina Narodytska, Joao Marques-Silva. 627-645 [doi]
- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL FunctionsSon Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish. 646-662 [doi]
- An Abstraction-Refinement Framework for Reasoning with Large TheoriesJulio Cesar Lopez Hernandez, Konstantin Korovin. 663-679 [doi]
- Efficient Model Construction for Horn Logic with VLog - System DescriptionJacopo Urbani, Markus Krötzsch, Ceriel J. H. Jacobs, Irina Dragoste, David Carral. 680-688 [doi]
- Focussing, \mathsf MALL and the Polynomial HierarchyAnupam Das. 689-705 [doi]
- Checking Array Bounds by Abstract Interpretation and Symbolic ExpressionsÉtienne Payet, Fausto Spoto. 706-722 [doi]