Abstract is missing.
- Mathematical Theory ExplorationBruno Buchberger. 1-2 [doi]
- Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge CompilationAdnan Darwiche. 3 [doi]
- Representing and Reasoning with Operational SemanticsDale Miller. 4-20 [doi]
- Flyspeck I: Tame GraphsTobias Nipkow, Gertrud Bauer, Paula Schultz. 21-35 [doi]
- Automatic Construction and Verification of Isotopy InvariantsVolker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton. 36-51 [doi]
- Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker AlgorithmsSylvie Boldo. 52-66 [doi]
- Using the TPTP Language for Writing Derivations and Finite InterpretationsGeoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder. 67-81 [doi]
- Stratified Context Unification Is NP-CompleteJordi Levy, Manfred Schmidt-Schauß, Mateu Villaret. 82-96 [doi]
- A Logical Characterization of Forward and Backward Chaining in the Inverse MethodKaustuv Chaudhuri, Frank Pfenning, Greg Price. 97-111 [doi]
- Connection Tableaux with Lazy ParamodulationAndrey Paskevich. 112-124 [doi]
- Blocking and Other Enhancements for Bottom-Up Model Generation MethodsPeter Baumgartner, Renate A. Schmidt. 125-139 [doi]
- The MathServe System for Semantic Web Reasoning ServicesJürgen Zimmer, Serge Autexier. 140-144 [doi]
- System Description: GCLCprover + GeoThmsPredrag Janicic, Pedro Quaresma. 145-150 [doi]
- A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo AxiomsJoe Hendrix, José Meseguer, Hitoshi Ohsaki. 151-155 [doi]
- Extending the TPTP Language to Higher-Order Logic with Automated Parser GenerationAllen Van Gelder, Geoff Sutcliffe. 156-161 [doi]
- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic SemanticsRobert L. Constable, Wojciech Moczydlowski. 162-176 [doi]
- Towards Self-verification of HOL LightJohn Harrison. 177-191 [doi]
- An Interpretation of Isabelle/HOL in HOL LightSean McLaughlin. 192-204 [doi]
- Combining Type Theory and Untyped Set TheoryChad E. Brown. 205-219 [doi]
- Cut-Simulation in Impredicative LogicsChristoph Benzmüller, Chad E. Brown, Michael Kohlhase. 220-234 [doi]
- Interpolation in Local Theory ExtensionsViorica Sofronie-Stokkermans. 235-250 [doi]
- Canonical Gentzen-Type Calculi with (n, k)-ary QuantifiersAnna Zamansky, Arnon Avron. 251-265 [doi]
- Dynamic Logic with Non-rigid FunctionsBernhard Beckert, André Platzer. 266-280 [doi]
- Automatic Termination Proofs in the Dependency Pair FrameworkJürgen Giesl, Peter Schneider-Kamp, René Thiemann. 281-286 [doi]
- CEL - A Polynomial-Time Reasoner for Life Science OntologiesFranz Baader, Carsten Lutz, Boontawee Suntisrivaraporn. 287-291 [doi]
- Description Logic Reasoner: System DescriptionDmitry Tsarkov, Ian Horrocks. 292-297 [doi]
- Importing HOL into Isabelle/HOLSteven Obua, Sebastian Skalberg. 298-302 [doi]
- Geometric Resolution: A Proof Procedure Based on Finite Model SearchHans de Nivelle, Jia Meng. 303-317 [doi]
- A Powerful Technique to Eliminate Isomorphism in Finite Model SearchXiangxue Jia, Jian Zhang. 318-331 [doi]
- Automation of Recursive Path Ordering for Infinite Labelled Rewrite SystemsAdam Koprowski, Hans Zantema. 332-346 [doi]
- Strong Cut-Elimination Systems for Hudelmaier s Depth-Bounded Sequent Calculus for Implicational LogicRoy Dyckhoff, Delia Kesner, Stéphane Lengrand. 347-361 [doi]
- Eliminating Redundancy in Higher-Order Unification: A Lightweight ApproachBrigitte Pientka. 362-376 [doi]
- First-Order Logic with Dependent TypesFlorian Rabe. 377-391 [doi]
- Automating Proofs in Category TheoryDexter Kozen, Christoph Kreitz, Eva Richter. 392-407 [doi]
- Formal Global Optimisation with Taylor ModelsRoland Zumkeller. 408-422 [doi]
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime NumbersBenjamin Grégoire, Laurent Théry. 423-437 [doi]
- Proving Formally the Implementation of an Efficient gcd Algorithm for PolynomialsAssia Mahboubi. 438-452 [doi]
- A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)Erik Reeber, Warren A. Hunt Jr.. 453-467 [doi]
- Solving Sparse Linear ConstraintsShuvendu K. Lahiri, Madanlal Musuvathi. 468-482 [doi]
- Inferring Network Invariants AutomaticallyOlga Grinchtein, Martin Leucker, Nir Piterman. 483-497 [doi]
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOLChristian Urban, Stefan Berghofer. 498-512 [doi]
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision ProceduresMaria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. 513-527 [doi]
- Verifying Mixed Real-Integer Quantifier EliminationAmine Chaieb. 528-540 [doi]
- Presburger Modal Logic Is PSPACE-CompleteStéphane Demri, Denis Lugiez. 541-556 [doi]
- Tree Automata with Equality Constraints Modulo Equational TheoriesFlorent Jacquemard, Michaël Rusinowitch, Laurent Vigneron. 557-571 [doi]
- CASC-J3 - The 3rd IJCAR ATP System CompetitionGeoff Sutcliffe. 572-573 [doi]
- Matrix Interpretations for Proving Termination of Term RewritingJörg Endrullis, Johannes Waldmann, Hans Zantema. 574-588 [doi]
- Partial Recursive Functions in Higher-Order LogicAlexander Krauss. 589-603 [doi]
- On the Strength of Proof-Irrelevant Type TheoriesBenjamin Werner. 604-618 [doi]
- Consistency and Completeness of Rewriting in the Calculus of ConstructionsDaria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz. 619-631 [doi]
- Specifying and Reasoning About Dynamic Access-Control PoliciesDaniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi. 632-646 [doi]
- On Keys and Functional Dependencies as First-Class Citizens in Description LogicsDavid Toman, Grant E. Weddell. 647-661 [doi]
- A Resolution-Based Decision Procedure for ::::SHOIQ::::Yevgeny Kazakov, Boris Motik. 662-677 [doi]