Abstract is missing.
- Games, Automata and MatchingColin Stirling. 1-2 [doi]
- Formalization of Continuous Probability DistributionsOsman Hasan, Sofiène Tahar. 3-18 [doi]
- Compilation as Rewriting in Higher Order LogicGuodong Li, Konrad Slind. 19-34 [doi]
- Barendregt s Variable Convention in Rule InductionsChristian Urban, Stefan Berghofer, Michael Norrish. 35-50 [doi]
- Automating Elementary Number-Theoretic Proofs Using Gröbner BasesJohn Harrison. 51-66 [doi]
- Optimized Reasoning in Description Logics Using HypertableauxBoris Motik, Rob Shearer, Ian Horrocks. 67-83 [doi]
- Conservative Extensions in the Lightweight Description Logic ELCarsten Lutz, Frank Wolter. 84-99 [doi]
- An Incremental Technique for Automata-Based Decision ProceduresGulay Ünel, David Toman. 100-115 [doi]
- Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4Samuli Heilala, Brigitte Pientka. 116-131 [doi]
- A Labelled System for IPL with Variable SplittingRoger Antonsen, Arild Waaler. 132-146 [doi]
- Logical Interpretation: Static Program Analysis Using Theorem ProvingAshish Tiwari, Sumit Gulwani. 147-166 [doi]
- Solving Quantified Verification Conditions Using Satisfiability Modulo TheoriesYeting Ge, Clark Barrett, Cesare Tinelli. 167-182 [doi]
- Efficient E-Matching for SMT SolversLeonardo Mendonça de Moura, Nikolaj Bjørner. 183-198 [doi]
- T-Decision by DecompositionMaria Paola Bonacina, Mnacho Echenim. 199-214 [doi]
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger ArithmeticViktor Kuncak, Martin C. Rinard. 215-230 [doi]
- Improvements in Formula GeneralizationMarkus Aderhold. 231-246 [doi]
- On the Normalization and Unique Normalization Properties of Term Rewrite SystemsGuillem Godoy, Sophie Tison. 247-262 [doi]
- Handling Polymorphism in Automated DeductionJean-Francois Couchot, Stéphane Lescuyer. 263-278 [doi]
- Automated Reasoning in Kleene AlgebraPeter Höfner, Georg Struth. 279-294 [doi]
- SRASS - A Semantic Relevance Axiom Selection SystemGeoff Sutcliffe, Yury Puzis. 295-310 [doi]
- Labelled ClausesTal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv. 311-327 [doi]
- Automatic Decidability and Combinability RevisitedChristopher Lynch, Duc-Khanh Tran. 328-344 [doi]
- Designing Verification Conditions for SoftwareK. Rustan M. Leino. 345 [doi]
- Encodings of Bounded LTL Model Checking in Effectively Propositional LogicJuan Antonio Navarro Pérez, Andrei Voronkov. 346-361 [doi]
- Combination Methods for Satisfiability and Model-Checking of Infinite-State SystemsSilvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. 362-378 [doi]
- The KeY system 1.0 (Deduction Component)Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt. 379-384 [doi]
- KeY-C: A Tool for Verification of C ProgramsOleg Mürk, Daniel Larsson, Reiner Hähnle. 385-390 [doi]
- The Bedwyr System for Model Checking over Syntactic ExpressionsDavid Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu. 391-397 [doi]
- System for Automated Deduction (SAD): A Tool for Proof VerificationKonstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich. 398-403 [doi]
- Logical Engineering with Instance-Based MethodsPeter Baumgartner. 404-409 [doi]
- Predictive Labeling with Dependency Pairs Using SATAdam Koprowski, Aart Middeldorp. 410-425 [doi]
- Dependency Pairs for Rewriting with Non-free ConstructorsStephan Falke, Deepak Kapur. 426-442 [doi]
- Proving Termination by Bounded IncreaseJürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp. 443-459 [doi]
- Certified Size-Change TerminationAlexander Krauss. 460-475 [doi]
- Encoding First Order Proofs in SATTodd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor. 476-491 [doi]
- Hyper Tableaux with EqualityPeter Baumgartner, Ulrich Furbach, Björn Pelzer. 492-507 [doi]
- System Description: E-KRHyperBjörn Pelzer, Christoph Wernhard. 508-513 [doi]
- System Description: SpassVersion 3.0Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic. 514-520 [doi]