Abstract is missing.
- Taking Satisfiability to the Next Level with Z3 - (Abstract)Nikolaj Bjørner. 1-8 [doi]
- Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in MathematicsYuri Matiyasevich. 9 [doi]
- SAT and SMT Are Still Resolution: Questions and ChallengesRobert Nieuwenhuis. 10-13 [doi]
- Unification Modulo Synchronous DistributivitySiva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch. 14-29 [doi]
- SAT Encoding of Unification in $\mathcal{ELH}_{{R}^+}$ w.r.t. Cycle-Restricted OntologiesFranz Baader, Stefan Borgwardt, Barbara Morawska. 30-44 [doi]
- UEL: Unification Solver for the Description Logic $\mathcal{EL}$ - System DescriptionFranz Baader, Julian Mendez, Barbara Morawska. 45-51 [doi]
- Effective Finite-Valued Semantics for Labelled CalculiMatthias Baaz, Ori Lahav, Anna Zamansky. 52-66 [doi]
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer ArithmeticFrançois Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond. 67-81 [doi]
- How Fuzzy Is My Fuzzy Description Logic?Stefan Borgwardt, Felix Distel, Rafael Peñaloza. 82-96 [doi]
- Truthful Monadic AbstractionsTaus Brock-Nannestad, Carsten Schürmann. 97-110 [doi]
- Satallax: An Automatic Higher-Order ProverChad E. Brown. 111-117 [doi]
- From Strong Amalgamability to Modularity of Quantifier-Free InterpolationRoberto Bruttomesso, Silvio Ghilardi, Silvio Ranise. 118-133 [doi]
- SPARQL Query Containment under RDFS Entailment RegimeMelisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda. 134-148 [doi]
- Automated Verification of Recursive Programs with PointersFrank S. de Boer, Marcello M. Bonsangue, Jurriaan Rot. 149-163 [doi]
- Security Protocols, Constraint Systems, and Group TheoriesStéphanie Delaune, Steve Kremer, Daniel Pasaila. 164-178 [doi]
- Taming Past LTL and Flat Counter SystemsStéphane Demri, Amit Kumar Dhar, Arnaud Sangnier. 179-193 [doi]
- A Calculus for Generating Ground ExplanationsMnacho Echenim, Nicolas Peltier. 194-209 [doi]
- EPR-Based Bounded Model Checking at Word LevelMoshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov. 210-224 [doi]
- Proving Non-looping Non-termination AutomaticallyFabian Emmes, Tim Enger, Jürgen Giesl. 225-240 [doi]
- Rewriting Induction + Linear Arithmetic = Decision ProcedureStephan Falke, Deepak Kapur. 241-255 [doi]
- Combination of Disjoint Theories: Beyond DecidabilityPascal Fontaine, Stephan Merz, Christoph Weidenbach. 256-270 [doi]
- Automated Analysis of Regular AlgebraSimon Foster, Georg Struth. 271-285 [doi]
- δ-Complete Decision Procedures for Satisfiability over the RealsSicun Gao, Jeremy Avigad, Edmund M. Clarke. 286-300 [doi]
- BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense LogicsRajeev Goré, Jimmy Thomson. 301-315 [doi]
- From Linear Temporal Logic Properties to Rewrite PropositionsPierre-Cyrille Héam, Vincent Hugot, Olga Kouchnarenko. 316-331 [doi]
- Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem ProverMélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois. 332-338 [doi]
- Solving Non-linear ArithmeticDejan Jovanovic, Leonardo Mendonça de Moura. 339-354 [doi]
- Inprocessing RulesMatti Järvisalo, Marijn Heule, Armin Biere. 355-370 [doi]
- Logical Difference Computation with CEX2.5Boris Konev, Michel Ludwig, Frank Wolter. 371-377 [doi]
- Overview and Evaluation of Premise Selection Techniques for Large Theory MathematicsDaniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes. 378-392 [doi]
- Branching Time? Pruning Time!Markus Latte, Martin Lange. 393-407 [doi]
- New Algorithms for Unification Modulo One-Sided Distributivity and Its VariantsAndrew M. Marshall, Paliath Narendran. 408-422 [doi]
- Reachability Analysis of Program VariablesDurica Nikolic, Fausto Spoto. 423-438 [doi]
- Playing Hybrid Games with KeYmaeraJan-David Quesel, André Platzer. 439-453 [doi]
- The QMLTP Problem Library for First-Order Modal LogicsThomas Raths, Jens Otten. 454-461 [doi]
- Correctness of Program Transformations as a Termination ProblemConrad Rau, David Sabel, Manfred Schmidt-Schauß. 462-476 [doi]
- Fingerprint Indexing for Paramodulation and RewritingStephan Schulz. 477-483 [doi]
- Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost FunctionsRoberto Sebastiani, Silvia Tomasi. 484-498 [doi]
- Synthesis for Unbounded Bit-Vector ArithmeticAndrej Spielmann, Viktor Kuncak. 499-513 [doi]
- Extended Caching, Backjumping and Merging for Expressive Description LogicsAndreas Steigmiller, Thorsten Liebig, Birte Glimm. 514-529 [doi]
- KBCV - Knuth-Bendix Completion VisualizerThomas Sternagel, Harald Zankl. 530-536 [doi]
- A PLTL-Prover Based on Labelled Superposition with Partial Model GuidanceMartin Suda, Christoph Weidenbach. 537-543 [doi]
- Stratification in Logics of DefinitionsAlwen Tiu. 544-558 [doi]
- Diabelli: A Heterogeneous Proof SystemMatej Urbas, Mateja Jamnik. 559-566 [doi]