Abstract is missing.
- Reasoning About Deductions in Linear Logic (Abstract of Invited Talk)Frank Pfenning. 1-2 [doi]
- A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton s PrincipiaJacques D. Fleuriot, Lawrence C. Paulson. 3-16 [doi]
- Proving Geometric Theorems Using Clifford Algebra and Rewrite RulesStéphane Fèvre, Dongming Wang. 17-31 [doi]
- System Description: Similarity-Based Lemma Generation for Model EliminationMarc Fuchs. 33-37 [doi]
- System Description: Verification of Distributed Erlang ProgramsThomas Arts, Mads Dam, Lars-Åke Fredlund, Dilian Gurov. 38-41 [doi]
- System Description: Cooperation in Model Elimination: CPTHEOMarc Fuchs, Andreas Wolf. 42-46 [doi]
- System Description: ::::card:::: ::::T:::::::::::A:::::::::::P::::: The First Theorem Prover on a Smart CardRajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt. 47-50 [doi]
- System Description: ::::lean::::K 2.0Bernhard Beckert, Rajeev Goré. 51-55 [doi]
- Extensional Higher-Order ResolutionChristoph Benzmüller, Michael Kohlhase. 56-71 [doi]
- X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order CalculiBruno Pagano. 72-87 [doi]
- About the Confluence of Equational Pattern Rewrite SystemsAlexandre Boudet, Evelyne Contejean. 88-102 [doi]
- Unification in Lambda-Calculi with if-then-elseMichael Beeson. 103-118 [doi]
- System Description: An Equational Constraints SolverNicolas Peltier. 119-123 [doi]
- System Description: CRIL Platform for SATBertrand Mazure, Lakhdar Sais, Éric Grégoire. 124-128 [doi]
- System Description: Proof Planning in Higher-Order Logic with Lambda-ClamJulian Richardson, Alan Smaill, Ian Green. 129-133 [doi]
- System Description: An Interface Between CL:::A:::M and HOLKonrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy. 134-138 [doi]
- System Description: LEO - A Higher-Order Theorem ProverChristoph Benzmüller, Michael Kohlhase. 139-144 [doi]
- Superposition for Divisible Torsion-Free Abelian GroupsUwe Waldmann. 144-159 [doi]
- Strict Basic SuperpositionLeo Bachmair, Harald Ganzinger. 160-174 [doi]
- Elimination of Equality via Transformation with Ordering ConstraintsLeo Bachmair, Harald Ganzinger, Andrei Voronkov. 175-190 [doi]
- A Resolution Decision Procedure for the Guarded FragmentHans de Nivelle. 191-204 [doi]
- Combining Hilbert Style and Semantic Reasoning in a Resolution FrameworkHans Jürgen Ohlbach. 205-219 [doi]
- ACL2 Support for Verification Projects (Invited Talk)Matt Kaufmann. 220-238 [doi]
- A Fast Algorithm for Uniform Semi-UnificationAlberto Oliart, Wayne Snyder. 239-253 [doi]
- Termination Analysis by Inductive EvaluationJürgen Brauburger, Jürgen Giesl. 254-269 [doi]
- Admissibility of Fixpoint Induction over Partial TypesKarl Crary. 270-285 [doi]
- Automated Theorem Proving in a Simple Meta-Logic for LFCarsten Schürmann, Frank Pfenning. 286-300 [doi]
- Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk)Amir Pnueli. 301 [doi]
- Automated Deduction of Finite-State Control Programs for Reactive SystemsRobi Malik. 302-316 [doi]
- A Proof Environment for the Development of Group Communication SystemsChristoph Kreitz, Mark Hayden, Jason Hickey. 317-332 [doi]
- On the Relationship Between Non-Horn Magic Sets and Relevancy TestingYoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa. 333-348 [doi]
- A Certified Version of Buchberger s AlgorithmLaurent Théry. 349-364 [doi]
- Selectively Instantiating DefinitionsMatthew Bishop, Peter B. Andrews. 365-380 [doi]
- Using Matings for Pruning Connection TableauxReinhold Letz. 381-396 [doi]
- On Generating Small Clause Normal FormsAndreas Nonnengart, Georg Rock, Christoph Weidenbach. 397-411 [doi]
- Rank/Activity: A Canonical Form for Binary ResolutionJoseph Douglas Horton, Bruce Spencer. 412-426 [doi]
- Towards Efficient SubsumptionTanel Tammet. 427-441 [doi]