Abstract is missing.
- Independently Checkable Proofs from Decision Procedures: Issues and ProgressAllen Van Gelder. 1 [doi]
- Zap: Automated Theorem Proving for Software AnalysisThomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi. 2-22 [doi]
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicToolsRobert Nieuwenhuis, Albert Oliveras. 23-46 [doi]
- Scaling Up: Computers vs. Common SenseDouglas B. Lenat. 47-47 [doi]
- A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding ProblemAlessandro Dal Palù, Agostino Dovier, Enrico Pontelli. 48-63 [doi]
- Disjunctive Constraint Lambda CalculiMatthias M. Hölzl, John N. Crossley. 64-78 [doi]
- Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search TreesYao Wu, Enrico Pontelli, Desh Ranjan. 79-94 [doi]
- The nomore++ Approach to Answer Set SolvingChristian Anger, Martin Gebser, Thomas Linke, André Neumann, Torsten Schaub. 95-109 [doi]
- Optimizing the Runtime Processing of Types in Polymorphic Logic Programming LanguagesGopalan Nadathur, Xiaochu Qi. 110-124 [doi]
- The Four Sons of PenroseNachum Dershowitz. 125-138 [doi]
- An Algorithmic Account of Ehrenfeucht Games on Labeled Successor StructuresAngelo Montanari, Alberto Policriti, Nicola Vitacolonna. 139-153 [doi]
- Second-Order Principles in Specification Languages for Object-Oriented ProgramsBernhard Beckert, Kerry Trentelman. 154-168 [doi]
- Strong Normalization of the Dual Classical Sequent CalculusDaniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec. 169-183 [doi]
- Termination of Fair Computations in Term RewritingSalvador Lucas, José Meseguer. 184-198 [doi]
- On Confluence of Infinitary Combinatory Reduction SystemsJeroen Ketema, Jakob Grue Simonsen. 199-214 [doi]
- Matching with Regular ConstraintsTemur Kutsia, Mircea Marin. 215-229 [doi]
- Recursive Path Orderings Can Also Be IncrementalMirtha-Lina Fernández, Guillem Godoy, Albert Rubio. 230-245 [doi]
- Automating Coherent LogicMarc Bezem, Thierry Coquand. 246-260 [doi]
- The Theorema Environment for Interactive Proof DevelopmentFlorina Piroi, Temur Kutsia. 261-275 [doi]
- A First Order Extension of Stålmarck s MethodMagnus Björk. 276-291 [doi]
- Regular Derivations in Basic Superposition-Based CalculiVladimir Aleksic, Anatoli Degtyarev. 292-306 [doi]
- On the Finite Satisfiability Problem for the Guarded Fragment with TransitivityWieslaw Szwast, Lidia Tendera. 307-321 [doi]
- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle EliminationChao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta. 322-336 [doi]
- Monotone AC-Tree AutomataHitoshi Ohsaki, Jean-Marc Talbot, Sophie Tison, Yves Roos. 337-351 [doi]
- On the Specification of Sequent SystemsElaine Pimentel, Dale Miller. 352-366 [doi]
- Verifying and Reflecting Quantifier Elimination for Presburger ArithmeticAmine Chaieb, Tobias Nipkow. 367-380 [doi]
- Integration of a Software Model Checker into IsabelleMatthias Daum, Stefan Maus, Norbert Schirmer, M. Nassim Seghir. 381-395 [doi]
- Experimental Evaluation of Classical Automata ConstructionsDeian Tabakov, Moshe Y. Vardi. 396-411 [doi]
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting SemanticsWolfgang Ahrendt, Andreas Roth, Ralf Sasse. 412-426 [doi]
- Reasoning About Incompletely Defined ProgramsChristoph Walther, Stephan Schweitzer. 427-442 [doi]
- Model Checking Abstract State Machines with Answer Set ProgrammingCalvin Kai Fan Tang, Eugenia Ternovska. 443-458 [doi]
- Characterizing Provability in Didier Galmiche, Daniel Méry. 459-473 [doi]
- A Unified Memory Model for PointersHarvey Tuch, Gerwin Klein. 474-488 [doi]
- Treewidth in Verification: Local vs. GlobalAndrea Ferrara, Guoqiang Pan, Moshe Y. Vardi. 489-503 [doi]
- Pushdown Module CheckingLaura Bozzelli, Aniello Murano, Adriano Peron. 504-518 [doi]
- Functional Correctness Proofs of Encryption AlgorithmsJianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang. 519-533 [doi]
- Towards Automated Proof Support for Probabilistic Distributed SystemsAnnabelle McIver, Tjark Weber. 534-548 [doi]
- Algebraic Intruder DeductionsDavid A. Basin, Sebastian Mödersheim, Luca Viganò. 549-564 [doi]
- Satisfiability Checking for PC(ID)Maarten Mariën, Rudradeb Mitra, Marc Denecker, Maurice Bruynooghe. 565-579 [doi]
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause LearningAllen Van Gelder. 580-594 [doi]
- Another Complete Local Search Method for SATHaiou Shen, Hantao Zhang. 595-605 [doi]
- Inference from Controversial ArgumentsSylvie Coste-Marquis, Caroline Devred, Pierre Marquis. 606-620 [doi]
- Programming Cognitive Agents in Defeasible LogicMehdi Dastani, Guido Governatori, Antonino Rotolo, Leendert W. N. van der Torre. 621-636 [doi]
- The Relationship Between Reasoning About Privacy and Default LogicsJürgen Dix, Wolfgang Faber, V. S. Subrahmanian. 637-650 [doi]
- Comparative Similarity, Tree Automata, and Diophantine EquationsMikhail Sheremet, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev. 651-665 [doi]
- Analytic Tableaux for KLM Preferential and Cumulative LogicsLaura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato. 666-681 [doi]
- Bounding Resource Consumption with Gödel-Dummett LogicsDominique Larchey-Wendling. 682-696 [doi]
- On Interpolation in Existence LogicsMatthias Baaz, Rosalie Iemhoff. 697-711 [doi]
- Incremental Integrity Checking: Limitations and PossibilitiesHenning Christiansen, Davide Martinenghi. 712-727 [doi]
- Concepts of Automata Construction from LTLCarsten Fritz. 728-742 [doi]