Abstract is missing.
- The Anatomy of Equinox - An Extensible Automated Reasoning Tool for First-Order Logic and Beyond - (Talk Abstract)Koen Claessen. 1-3 [doi]
- Advances in Proving Program Termination and LivenessByron Cook. 4 [doi]
- Translating between Language and Logic: What Is Easy and What Is DifficultAarne Ranta. 5-25 [doi]
- ASASP: Automated Symbolic Analysis of Security PoliciesFrancesco Alberti, Alessandro Armando, Silvio Ranise. 26-33 [doi]
- Backward Trace Slicing for Rewriting Logic TheoriesMaría Alpuente, Demis Ballis, Javier Espert, Daniel Romero. 34-48 [doi]
- Deciding Security for Protocols with Recursive TestsMathilde Arnaud, Véronique Cortier, Stéphanie Delaune. 49-63 [doi]
- The Matita Interactive Theorem ProverAndrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. 64-69 [doi]
- Unification in the Description Logic ::::EL::::/mathcal{EL} without the Top ConceptFranz Baader, Nguyen Thanh Binh, Stefan Borgwardt, Barbara Morawska. 70-84 [doi]
- Model Evolution with Equality Modulo Built-in TheoriesPeter Baumgartner, Cesare Tinelli. 85-100 [doi]
- Blocked Clause Elimination for QBFArmin Biere, Florian Lonsing, Martina Seidl. 101-115 [doi]
- Extending Sledgehammer with SMT SolversJasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson. 116-130 [doi]
- Automated Cyclic Entailment Proofs in Separation LogicJames Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen. 131-146 [doi]
- Reducing Higher-Order Theorem Proving to a Sequence of SAT ProblemsChad E. Brown. 147-161 [doi]
- Experimenting with Deduction ModuloGuillaume Burel. 162-176 [doi]
- Heaps and Data Structures: A Challenge for Automated ProversSascha Böhme, Michal Moskal. 177-191 [doi]
- Optimized Query Rewriting for OWL 2 QLAlexandros Chortaras, Despoina Trivela, Giorgos B. Stamou. 192-206 [doi]
- Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order LogicKoen Claessen, Ann Lillieström, Nicholas Smallbone. 207-221 [doi]
- Exploiting Symmetry in SMT ProblemsDavid Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. 222-236 [doi]
- Compression of Propositional Resolution Proofs via Partial RegularizationPascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. 237-251 [doi]
- Dynamic Behavior Matching: A Complexity Analysis and New Approximation AlgorithmsMatthew Fredrikson, Mihai Christodorescu, Somesh Jha. 252-267 [doi]
- A Connection-Based Characterization of Bi-intuitionistic ValidityDidier Galmiche, Daniel Méry. 268-282 [doi]
- Automated Reasoning in ::::ALCQ::::/mathcal{ALCQ} via SMTVolker Haarslev, Roberto Sebastiani, Michele Vescovi. 283-298 [doi]
- Sine Qua Non for Large Theory ReasoningKrystof Hoder, Andrei Voronkov. 299-314 [doi]
- Predicate Completion for non-Horn Clause SetsMatthias Horbach. 315-330 [doi]
- System Description: SPASS-FDMatthias Horbach. 331-337 [doi]
- Cutting to the Chase Solving Linear Integer ArithmeticDejan Jovanovic, Leonardo Mendonça de Moura. 338-353 [doi]
- A Hybrid Method for Probabilistic SatisfiabilityPavel Klinov, Bijan Parsia. 354-368 [doi]
- Solving Systems of Linear Inequalities by Bound PropagationKonstantin Korovin, Andrei Voronkov. 369-383 [doi]
- On Transfinite Knuth-Bendix OrdersLaura Kovács, Georg Moser, Andrei Voronkov. 384-399 [doi]
- Scala to the Power of Z3: Integrating SMT and ProgrammingAli Sinan Köksal, Viktor Kuncak, Philippe Suter. 400-406 [doi]
- Efficient General Unification for XOR with HomomorphismZhiqiang Liu, Christopher Lynch. 407-421 [doi]
- A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite SystemsLars Noschinski, Fabian Emmes, Jürgen Giesl. 422-438 [doi]
- Static Analysis of Android ProgramsÉtienne Payet, Fausto Spoto. 439-445 [doi]
- Stochastic Differential Dynamic Logic for Stochastic Hybrid ProgramsAndré Platzer. 446-460 [doi]
- Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem ProvingMichael Schneider, Geoff Sutcliffe. 461-475 [doi]
- An Efficient Decision Procedure for Imperative Tree Data StructuresThomas Wies, Marco Muñiz, Viktor Kuncak. 476-491 [doi]
- AC Completion with Termination ToolsSarah Winkler, Aart Middeldorp. 492-498 [doi]
- CSI - A Confluence ToolHarald Zankl, Bertram Felgenhauer, Aart Middeldorp. 499-505 [doi]