Table of Contents

• From Reachability to Temporal Specifications in Cost-Sharing GamesGuy Avni, Orna Kupferman, Tami Tamir. 1-15 [doi]
• Electronic Voting: How Logic Can HelpVéronique Cortier. 16-25 [doi]
• And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDLRajeev Goré. 26-45 [doi]
• Unified Classical Logic Completeness - A Coinductive PearlJasmin Christian Blanchette, Andrei Popescu 0001, Dmitriy Traytel. 46-60 [doi]
• A Focused Sequent Calculus for Higher-Order LogicFredrik Lindblad. 61-75 [doi]
• SAT-Based Decision Procedure for Analytic Pure Sequent CalculiOri Lahav, Yoni Zohar. 76-90 [doi]
• A Unified Proof System for QBF PreprocessingMarijn Heule, Martina Seidl, Armin Biere. 91-106 [doi]
• The Fractal Dimension of SAT FormulasCarlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy. 107-121 [doi]
• A Gentle Non-disjoint Combination of Satisfiability ProceduresPaula Chocron, Pascal Fontaine, Christophe Ringeissen. 122-136 [doi]
• A Rewriting Strategy to Generate Prime Implicates in Equational LogicMnacho Echenim, Nicolas Peltier, Sophie Tourret. 137-151 [doi]
• Finite Quantification in Hierarchic Theorem ProvingPeter Baumgartner, Joshua Bax, Uwe Waldmann. 152-167 [doi]
• Computing All Implied Equalities via SMT-Based Partition RefinementJosh Berdine, Nikolaj Bjørner. 168-183 [doi]
• Proving Termination of Programs Automatically with AProVEJürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann. 184-191 [doi]
• Locality Transfer: From Constrained Axiomatizations to Reachability PredicatesMatthias Horbach, Viorica Sofronie-Stokkermans. 192-207 [doi]
• Proving Termination and Memory Safety for Programs with Pointer ArithmeticThomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp. 208-223 [doi]
• QBF Encoding of Temporal Properties and QBF-Based VerificationWenhui Zhang. 224-239 [doi]
• Introducing Quantified Cuts in Logic with EqualityStefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller. 240-254 [doi]
• Quati: An Automated Tool for Proving Permutation LemmasVivek Nigam, Giselle Reis, Leonardo Lima. 255-261 [doi]
• A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System DescriptionRajeev Goré, Jimmy Thomson, Jesse Wu. 262-268 [doi]
• MleanCoP: A Connection Prover for First-Order Modal LogicJens Otten. 269-276 [doi]
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+Serenella Cerrito, Amélie David, Valentin Goranko. 277-291 [doi]
• dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid SystemsJean-Baptiste Jeannin, André Platzer. 292-306 [doi]
• Axioms vs Hypersequent Rules with Context Restrictions: Theory and ApplicationsBjörn Lellmann. 307-321 [doi]
• Clausal Resolution for Modal Logics of ConfluenceCláudia Nalon, João Marcos, Clare Dixon. 322-336 [doi]
• Implementing Tableau Calculi Using BDDs: BDDTab System DescriptionRajeev Goré, Kerry Olesen, Jimmy Thomson. 337-343 [doi]
• Approximations for Model ConstructionAleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer. 344-359 [doi]
• A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal LogicRüdiger Ehlers, Martin Lange. 360-366 [doi]
• StarExec: A Cross-Community Infrastructure for Logic SolvingAaron Stump, Geoff Sutcliffe, Cesare Tinelli. 367-373 [doi]
• Skeptik: A Proof Compression SystemJoseph Boudou, Andreas Fellner, Bruno Woltzenlogel Paleo. 374-380 [doi]
• Terminating Minimal Model Generation Procedures for Propositional Modal LogicsFabio Papacchini, Renate A. Schmidt. 381-395 [doi]
• Cool - A Generic Reasoner for Coalgebraic Hybrid Logics (System Description)Daniel Gorín, Dirk Pattinson, Lutz Schröder, Florian Widmann, Thorsten Wißmann. 396-402 [doi]
• The Complexity of Theorem Proving in Circumscription and Minimal EntailmentOlaf Beyersdorff, Leroy Chew. 403-417 [doi]
• Visibly Linear Temporal LogicLaura Bozzelli, César Sánchez. 418-433 [doi]
• Count and Forget: Uniform Interpolation of $\mathcal{SHQ}$ -OntologiesPatrick Koopmann, Renate A. Schmidt. 434-448 [doi]
• Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation ProceduresAndreas Steigmiller, Birte Glimm, Thorsten Liebig. 449-463 [doi]
• EL-ifying OntologiesDavid Carral Martínez, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler, Ian Horrocks. 464-479 [doi]
• The Bayesian Description Logic ${\mathcal{BEL}}$Ismail Ilkan Ceylan, Rafael Peñaloza. 480-494 [doi]
• OTTER Proofs in Tarskian GeometryMichael Beeson, Larry Wos. 495-510 [doi]
• NESCOND: An Implementation of Nested Sequent Calculi for Conditional LogicsNicola Olivetti, Gian Luca Pozzato. 511-518 [doi]
• Knowledge Engineering for Large Ontologies with Sigma KEE 3.0Adam Pease, Stephan Schulz. 519-525 [doi]