Abstract is missing.
- Reasoning with Expressive Description Logics: Theory and PracticeIan Horrocks. 1-15 [doi]
- BDD-Based Decision Procedures for KGuoqiang Pan, Ulrike Sattler, Moshe Y. Vardi. 16-30 [doi]
- Temporal Logic for Proof-Carrying CodeAndrew Bernard, Peter Lee. 31-46 [doi]
- A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying CodeRobert R. Schneck, George C. Necula. 47-62 [doi]
- Formal Verification of a Java Compiler in IsabelleMartin Strecker. 63-77 [doi]
- Embedding Lax Logic into Intuitionistic LogicUwe Egly. 78-93 [doi]
- Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett LogicDominique Larchey-Wendling. 94-110 [doi]
- Connection-Based Proof Search in Propositional BI LogicDidier Galmiche, Daniel Méry. 111-128 [doi]
- DDDLIB: A Library for Solving Quantified Difference InequalitiesJesper B. Møller. 129-133 [doi]
- An LCF-Style Interface between HOL and First-Order LogicJoe Hurd. 134-138 [doi]
- System Description: The MathWeb Software Bus for Distributed Mathematical ReasoningJürgen Zimmer, Michael Kohlhase. 139-143 [doi]
- Proof Development with OMEGAJörg H. Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jürgen Zimmer. 144-149 [doi]
- Learn Omega-matic: System DescriptionMateja Jamnik, Manfred Kerber, Martin Pollet. 150-155 [doi]
- HyLoRes 1.0: Direct Resolution for Hybrid LogicsCarlos Areces, Juan Heguiabehere. 156-160 [doi]
- Testing Satisfiability of CNF Formulas by Computing a Stable Set of PointsEugene Goldberg. 161-180 [doi]
- A Note on Symmetry Heuristics in SEMThierry Boy de la Tour. 181-194 [doi]
- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical PropositionsGilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. 195-210 [doi]
- Deductive Search for Errors in Free Data Type Specifications Using Model GenerationWolfgang Ahrendt. 211-225 [doi]
- Reasoning by Symmetry and Function Ordering in Finite Model GenerationGilles Audemard, Belaid Benhamou. 226-240 [doi]
- Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground EquationsBernhard Gramlich, Reinhard Pichler. 241-259 [doi]
- A New Clausal Class Decidable by HyperresolutionLilia Georgieva, Ullrich Hustadt, Renate A. Schmidt. 260-274 [doi]
- S PASS Version 2.0Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobald, Dalibor Topic. 275-279 [doi]
- System Description: GrAnDe 1.0Stephan Schulz, Geoff Sutcliffe. 280-284 [doi]
- The HR Program for Theorem GenerationSimon Colton. 285-289 [doi]
- AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System DescriptionMichael W. Whalen, Johann Schumann, Bernd Fischer. 290-294 [doi]
- The Quest for Efficient Boolean Satisfiability SolversLintao Zhang, Sharad Malik. 295-313 [doi]
- Recursive Path Orderings Can Be Context-SensitiveCristina Borralleras, Salvador Lucas, Albert Rubio. 314-331 [doi]
- Shostak LightHarald Ganzinger. 332-346 [doi]
- Formal Verification of a Combination Decision ProcedureJonathan Ford, Natarajan Shankar. 347-362 [doi]
- Combining Multisets with IntegersCalogero G. Zarba. 363-376 [doi]
- The Reflection Theorem: A Study in Meta-theoretic ReasoningLawrence C. Paulson. 377-391 [doi]
- Faster Proof Checking in the Edinburgh Logical FrameworkAaron Stump, David L. Dill. 392-407 [doi]
- Solving for Set Variables in Higher-Order Theorem ProvingChad E. Brown. 408-422 [doi]
- The Complexity of the Graded µ-CalculusOrna Kupferman, Ulrike Sattler, Moshe Y. Vardi. 423-437 [doi]
- Lazy Theorem Proving for Bounded Model Checking over Infinite DomainsLeonardo Mendonça de Moura, Harald Rueß, Maria Sorea. 438-455 [doi]
- Well-Foundedness Is Sufficient for Completeness of Ordered ParamodulationMiquel Bofill, Albert Rubio. 456-470 [doi]
- Basic Syntactic MutationChristopher Lynch, Barbara Morawska. 471-485 [doi]
- The Next W ALDMEISTER LoopThomas Hillenbrand, Bernd Löchner. 486-500 [doi]
- Focussing Proof-Net Construction as a Middleware ParadigmJean-Marc Andreoli. 501-516 [doi]
- Proof Analysis by ResolutionMatthias Baaz. 517-532 [doi]