Abstract is missing.
- Unification Modulo Lists with Reverse Relation with Certain Word EquationsSiva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch. 1-17 [doi]
- On the Width of Regular Classes of Finite StructuresAlexsander Andrade de Melo, Mateus de Oliveira Oliveira. 18-34 [doi]
- Extending SMT Solvers to Higher-Order LogicHaniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett. 35-54 [doi]
- Superposition with LambdasAlexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann. 55-73 [doi]
- Restricted Combinatory UnificationAhmed Bhayat, Giles Reger. 74-93 [doi]
- ι: Definite Descriptions in Differential Dynamic LogicBrandon Bohrer, Manuel Fernández, André Platzer. 94-110 [doi]
- SPASS-SATT - A CDCL(LA) SolverMartin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach. 111-122 [doi]
- GRUNGE: A Grand Unified ATP ChallengeChad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban. 123-141 [doi]
- Model Completeness, Covers and SuperpositionDiego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin. 142-160 [doi]
- A Tableaux Calculus for Default Intuitionistic LogicValentin Cassano, Raul Fervari, Guillaume Hoffmann, Carlos Areces, Pablo F. Castro. 161-177 [doi]
- NIL: Learning Nonlinear InterpolantsMingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan. 178-196 [doi]
- ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for EKarel Chvalovský, Jan Jakubuv, Martin Suda 0001, Josef Urban. 197-215 [doi]
- Towards Physical Hybrid SystemsKatherine Cordwell, André Platzer. 216-232 [doi]
- SCL Clause Learning from Simple ModelsAlberto Fiori, Christoph Weidenbach. 233-249 [doi]
- Names Are Not Just Sound and Smoke: Word Embeddings for Axiom SelectionUlrich Furbach, Teresa Krämer, Claudia Schon. 250-268 [doi]
- Computing Expected Runtimes for Constant Probability ProgramsJürgen Giesl, Peter Giesl, Marcel Hark. 269-286 [doi]
- Automatic Generation of Logical Models with AGESRaúl Gutiérrez, Salvador Lucas. 287-299 [doi]
- Automata Terms in a Lazy WSkS Decision ProcedureVojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar. 300-318 [doi]
- Confluence by Critical Pair Analysis RevisitedNao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi. 319-336 [doi]
- Composing Proof TermsChristina Kohl, Aart Middeldorp. 337-353 [doi]
- Combining ProVerif and Automated Theorem Provers for Security Protocol VerificationDi Long Li, Alwen Tiu. 354-365 [doi]
- Towards Bit-Width-Independent Proofs in SMT SolversAina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli. 366-384 [doi]
- On Invariant Synthesis for Parametric SystemsDennis Peuter, Viorica Sofronie-Stokkermans. 385-405 [doi]
- The Aspect CalculusDavid A. Plaisted. 406-424 [doi]
- Uniform Substitution at One Fell SwoopAndré Platzer. 425-441 [doi]
- A Formally Verified Abstract Account of Gödel's Incompleteness TheoremsAndrei Popescu 0001, Dmitriy Traytel. 442-461 [doi]
- Old or Heavy? Decaying Gracefully with Age/Weight ShapesMichael Rawson, Giles Reger. 462-476 [doi]
- Induction in Saturation-Based Proof SearchGiles Reger, Andrei Voronkov. 477-494 [doi]
- Faster, Higher, Stronger: E 2.3Stephan Schulz 0001, Simon Cruanes, Petar Vukmirovic. 495-507 [doi]
- Certified Equational Reasoning via Ordered CompletionChristian Sternagel, Sarah Winkler. 508-525 [doi]
- JGXYZ: An ATP System for Gap and Glut LogicsGeoff Sutcliffe, Francis Jeffry Pelletier. 526-537 [doi]
- GKC: A Reasoning System for Large Knowledge BasesTanel Tammet. 538-549 [doi]
- Optimization Modulo the Theory of Floating-Point NumbersPatrick Trentin, Roberto Sebastiani. 550-567 [doi]
- FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number RestrictionsYizheng Zhao, Renate A. Schmidt. 568-579 [doi]