Abstract is missing.
- History and Prospects for First-Order Automated DeductionDavid A. Plaisted. 3-28 [doi]
- Stumbling Around in the Dark: Lessons from Everyday MathematicsUrsula Martin. 29-51 [doi]
- Automated Reasoning in the WildUlrich Furbach, Björn Pelzer, Claudia Schon. 55-72 [doi]
- Automating Leibniz's Theory of ConceptsJesse Alama, Paul E. Oppenheimer, Edward N. Zalta. 73-97 [doi]
- Confluence Competition 2015Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida 0001, Harald Zankl. 101-104 [doi]
- Termination Competition (termCOMP 2015)Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann. 105-108 [doi]
- Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are ConfluentMasahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa. 111-126 [doi]
- CoLL: A Confluence Tool for Left-Linear Term Rewrite SystemsKiraku Shintani, Nao Hirokawa. 127-136 [doi]
- Term Rewriting with Prefix Context Constraints and Bottom-Up StrategiesFlorent Jacquemard, Yoshiharu Kojima, Masahiko Sakai. 137-151 [doi]
- Encoding Dependency Pair Techniques and Control Strategies for Maximal CompletionHaruhiko Sato, Sarah Winkler. 152-162 [doi]
- Reducing Relative Termination to Dependency Pair ProblemsJosé Iborra, Naoki Nishida 0001, Germán Vidal, Akihisa Yamada. 163-178 [doi]
- Decidability of Univariate Real Algebra with Predicates for Rational and Integer PowersGrant Olney Passmore. 181-196 [doi]
- A Decision Procedure for (Co)datatypes in SMT SolversAndrew Reynolds, Jasmin Christian Blanchette. 197-213 [doi]
- Deciding \mathsf ATL^* Satisfiability by TableauxAmélie David. 214-228 [doi]
- A Formalisation of Finite Automata Using Hereditarily Finite SetsLawrence C. Paulson. 231-245 [doi]
- SEPIA: Search for Proofs Using Inferred AutomataThomas Gransden, Neil Walkinshaw, Rajeev Raman. 246-255 [doi]
- Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3Filip Maric, Predrag Janicic, Marko Malikovic. 256-271 [doi]
- Inductive Beluga: Programming ProofsBrigitte Pientka, Andrew Cave. 272-281 [doi]
- SMTtoTPTP - A Converter for Theorem Proving FormatsPeter Baumgartner. 285-294 [doi]
- CTL Model Checking in Deduction ModuloKailiang Ji. 295-310 [doi]
- Quantifier-Free Equational Logic and Prime Implicate GenerationMnacho Echenim, Nicolas Peltier, Sophie Tourret. 311-325 [doi]
- Quantomatic: A Proof Assistant for Diagrammatic ReasoningAleks Kissinger, Vladimir Zamdzhiev. 326-336 [doi]
- Cooperating Proof AttemptsGiles Reger, Dmitry Tishkovsky, Andrei Voronkov. 339-355 [doi]
- Towards the Compression of First-Order Resolution Proofs by Lowering Unit ClausesJan Gorzny, Bruno Woltzenlogel Paleo. 356-366 [doi]
- Beagle - A Hierarchic Superposition Theorem ProverPeter Baumgartner, Joshua Bax, Uwe Waldmann. 367-377 [doi]
- The Lean Theorem Prover (System Description)Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer. 378-388 [doi]
- System Description: E.T. 0.1Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil. 389-398 [doi]
- Playing with AVATARGiles Reger, Martin Suda 0001, Andrei Voronkov. 399-415 [doi]
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions RevisitedPaula Chocron, Pascal Fontaine, Christophe Ringeissen. 419-433 [doi]
- Exploring Theories with a Model-Finding AssistantSalman Saghafi, Ryan Danas, Daniel J. Dougherty. 434-449 [doi]
- Abstract Interpretation as Automated DeductionVijay D'Silva, Caterina Urban. 450-464 [doi]
- A Uniform Substitution Calculus for Differential Dynamic LogicAndré Platzer. 467-481 [doi]
- Program Synthesis Using Dual InterpretationAshish Tiwari, Adria Gascón, Bruno Dutertre. 482-497 [doi]
- Automated Theorem Proving for Assertions in Separation Logic with All ConnectivesZhe Hou, Rajeev Goré, Alwen Tiu. 501-516 [doi]
- KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABSCrystal Chang Din, Richard Bubel, Reiner Hähnle. 517-526 [doi]
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid SystemsNathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer. 527-538 [doi]
- Tableaux Methods for Propositional Dynamic Logics with Separating Parallel CompositionPhilippe Balbiani, Joseph Boudou. 539-554 [doi]
- Regular Patterns in Second-Order UnificationTomer Libal. 557-571 [doi]
- Theorem Proving with Bounded Rigid E-UnificationPeter Backeman, Philipp Rümmer. 572-587 [doi]
- Expressing Symmetry Breaking in DRAT ProofsMarijn Heule, Warren A. Hunt Jr., Nathan Wetzler. 591-606 [doi]
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT SolversEdward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki. 607-622 [doi]
- Linear Integer Arithmetic RevisitedMartin Bromberger, Thomas Sturm 0001, Christoph Weidenbach. 623-637 [doi]