Abstract is missing.
- An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal LogicsLuca Aceto, Dario Della Monica, Anna Ingólfsdóttir, Angelo Montanari, Guido Sciavicco. 1-17 [doi]
- May-Happen-in-Parallel Analysis for Priority-Based SchedulingElvira Albert, Samir Genaim, Enrique Martin-Martin. 18-34 [doi]
- The Complexity of Clausal Fragments of LTLAlessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, Michael Zakharyaschev. 35-52 [doi]
- A Semantic Basis for Proof Queries and TransformationsDavid Aspinall, Ewen Denney, Christoph Lüth. 53-70 [doi]
- Expressive Path Queries on Graphs with DataPablo Barceló, Gaëlle Fontaine, Anthony Widjaja Lin. 71-85 [doi]
- Proving Infinite SatisfiabilityPeter Baumgartner, Joshua Bax. 86-95 [doi]
- SAT-Based Preprocessing for MaxSATAnton Belov, António Morgado, Joao Marques-Silva. 96-111 [doi]
- Dynamic and Static Symmetry Breaking in Answer Set ProgrammingBelaid Benhamou. 112-126 [doi]
- HOL Based First-Order Modal Logic ProversChristoph Benzmüller, Thomas Raths. 127-136 [doi]
- Resourceful Reachability as HORN-LAJosh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger. 137-146 [doi]
- A Seligman-Style Tableau SystemPatrick Blackburn, Thomas Bolander, Torben Braüner, Klaus Frovin Jørgensen. 147-163 [doi]
- Comparison of LTL to Deterministic Rabin Automata TranslatorsFrantisek Blahoudek, Mojmír Kretínský, Jan Strejcek. 164-172 [doi]
- Tree Interpolation in VampireRégis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl. 173-181 [doi]
- Polarizing Double-Negation TranslationsMélanie Boudard, Olivier Hermant. 182-197 [doi]
- Revisiting the Equivalence of Shininess and PolitenessFilipe Casal, João Rasga. 198-212 [doi]
- Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel LogicGiovanni Casini, Umberto Straccia. 213-227 [doi]
- Multi-objective Discounted Reward Verification in Graphs and MDPsKrishnendu Chatterjee, Vojtech Forejt, Dominik Wojtczak. 228-242 [doi]
- Description Logics, Rules and Multi-context SystemsLuís Cruz-Filipe, Rita Henriques, Isabel Nunes. 243-257 [doi]
- Complexity Analysis in Presence of Control Operators and Higher-Order FunctionsUgo Dal Lago, Giulio Pellitta. 258-273 [doi]
- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction ModuloDavid Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. 274-290 [doi]
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF SolvingUwe Egly, Florian Lonsing, Magdalena Widl. 291-308 [doi]
- Verifying Temporal Properties in Real ModelsTim French, John Christopher McCabe-Dansted, Mark Reynolds. 309-323 [doi]
- A Graphical Language for Proof StrategiesGudmund Grov, Aleks Kissinger, Yuhui Lin. 324-339 [doi]
- A Proof of Strong Normalisation of the Typed Atomic Lambda-CalculusTom Gundersen, Willem Heijltjes, Michel Parigot. 340-354 [doi]
- Relaxing Synchronization Constraints in Behavioral ProgramsDavid Harel, Amir Kantor, Guy Katz. 355-372 [doi]
- Characterizing Subset Spaces as Bi-topological StructuresBernhard Heinemann. 373-388 [doi]
- Proof-Pattern Recognition and Lemma Discovery in ACL2Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean. 389-406 [doi]
- Semantic A-translations and Super-Consistency Entail Classical Cut EliminationLisa Allali, Olivier Hermant. 407-422 [doi]
- Blocked Clause DecompositionMarijn Heule, Armin Biere. 423-438 [doi]
- Maximal Falsifiability - Definitions, Algorithms, and ApplicationsAlexey Ignatiev, António Morgado, Jordi Planes, Joao Marques-Silva. 439-456 [doi]
- Solving Geometry Problems Using a Combination of Symbolic and Numerical ReasoningShachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv. 457-472 [doi]
- On QBF Proofs and PreprocessingMikolás Janota, Radu Grigore, Joao Marques-Silva. 473-489 [doi]
- Partial Backtracking in CDCL SolversChuan Jiang, Ting Zhang. 490-502 [doi]
- Lemma Mining over HOL LightCezary Kaliszyk, Josef Urban. 503-517 [doi]
- On Module-Based Abstraction and Repair of Behavioral ProgramsGuy Katz. 518-535 [doi]
- Prediction and Explanation over DL-Lite Data StreamsSzymon Klarman, Thomas Meyer. 536-551 [doi]
- Forgetting Concept and Role Symbols in $\mathcal{ALCH}$ -OntologiesPatrick Koopmann, Renate A. Schmidt. 552-567 [doi]
- Simulating Parity ReasoningTero Laitinen, Tommi A. Junttila, Ilkka Niemelä. 568-583 [doi]
- Herbrand Theorems for Substructural LogicsPetr Cintula, George Metcalfe. 584-600 [doi]
- On Promptness in Parity GamesFabio Mogavero, Aniello Murano, Loredana Sorrentino. 601-618 [doi]
- Defining Privacy Is Supposed to Be EasySebastian Mödersheim, Thomas Groß, Luca Viganò. 619-635 [doi]
- Reachability Modules for the Description Logic $\mathcal{SRIQ}$Riku Nortje, Katarina Britz, Thomas Meyer. 636-652 [doi]
- An Event Structure Model for Probabilistic Concurrent Kleene AlgebraAnnabelle McIver, Tahiry M. Rabehaja, Georg Struth. 653-667 [doi]
- Three SCC-Based Emptiness Checks for Generalized Büchi AutomataEtienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud. 668-682 [doi]
- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software VerificationSimone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina. 683-693 [doi]
- Incremental Tabling for Query-Driven Propagation of Logic Program UpdatesAri Saptawijaya, Luís Moniz Pereira. 694-709 [doi]
- Tracking Data-Flow with Open Closure TypesGabriel Scherer, Jan Hoffmann. 710-726 [doi]
- Putting Newton into Practice: A Solver for Polynomial Equations over SemiringsMaximilian Schlund, Michal Terepeta, Michael Luttenberger. 727-734 [doi]
- System Description: E 1.8Stephan Schulz. 735-743 [doi]
- Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-LightSyeda Hira Taqdees, Osman Hasan. 744-758 [doi]
- On Minimality and Integrity Constraints in Probabilistic AbductionCalin-Rares Turliuc, Nataly Maimari, Alessandra Russo, Krysia Broda. 759-775 [doi]
- Polar: A Framework for Proof RefactoringDominik Dietrich, Iain Whiteside, David Aspinall. 776-791 [doi]