Front matter
1-2
Reasoning about deductions in linear logic
Frank Pfenning
3-16
A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia
Jacques D. Fleuriot and Lawrence C. Paulson
17-32
Proving geometric theorems using clifford algebra and rewrite rules
Stéphane Fèvre and Dongming Wang
33-37
System description: similarity-based lemma generation for model elimination
Marc Fuchs
38-41
System description: Verification of distributed Erlang programs
Thomas Arts, Mads Dam, Lars -åke Fredlund and Dilian Gurov
42-46
System description: Cooperation in model elimination: CPTHEO
Marc Fuchs and Andreas Wolf
47-50
System description: CardTAP: The first theorem prover on a smart card
Rajeev Goré, Joachim Posegga, Andrew Slater and Harald Vogt
51-55
System description: leanK 2.0
Bernhard Beckert and Rajeev Goré
56-71
Extensional higher-order resolution
Christoph Benzmüller and Michael Kohlhase
72-87
X.R.S: Explicit reduction systems — A first-order calculus for higher-order calculi
Bruno Pagano
88-102
About the confluence of equational pattern rewrite systems
Alexandre Boudet and Evelyne Contejean
103-118
Unification in lambda-calculi with if-then-else
Michael Beeson
119-123
System description: An equational constraints solver
Nicolas Peltier
124-128
System description: CRIL platform for SAT
Bertrand Mazure, Lakhdar SaÏs and éric Grégoire
129-133
System description: Proof planning in higher-order logic with λClam
Julian Richardson, Alan Smaill and Ian Green
134-138
System description: An interface between CLAM and HOL
Konrad Slind, Mike Gordon, Richard Boulton and Alan Bundy
139-143
System description: Leo — A higher-order theorem prover
Christoph Benzmüller and Michael Kohlhase
144-159
Superposition for divisible torsion-free abelian groups
Uwe Waldmann
160-174
Strict basic superposition
Leo Bachmair and Harald Ganzinger
175-190
Elimination of equality via transformation with ordering constraints
Leo Bachmair, Harald Ganzinger and Andrei Voronkov
191-204
A resolution decision procedure for the guarded fragment
Hans de Nivelle
205-219
Combining Hilbert style and semantic reasoning in a resolution framework
Hans Jürgen Ohlbach
220-238
ACL2 support for verification projects
Matt Kaufmann
239-253
A fast algorithm for uniform semi-unification
Alberto Oliart and Wayne Snyder
254-269
Termination analysis by inductive evaluation
Jürgen Brauburger and Jürgen Giesl
270-285
Admissibility of fixpoint induction over partial types
Karl Crary
286-300
Automated theorem proving in a simple meta-logic for LF
Carsten Schürmann and Frank Pfenning
301
Deductive vs. model-theoretic approaches to formal verification
Amir Pnueli
302-316
Automated deduction of finite-state control programs for reactive systems
Robi Malik
317-332
A proof environment for the development of group communication systems
Christoph Kreitz, Mark Hayden and Jason Hickey
333-348
On the relationship between non-horn magic sets and relevancy testing
Yoshihiko Ohta, Katsumi Inoue and Ryuzo Hasegawa
349-364
Certified version of Buchberger's algorithm
Laurent Théry
365-380
Selectively instantiating definitions
Matthew Bishop and Peter B. Andrews
381-396
Using matings for pruning connection tableaux
Reinhold Letz
397-411
On generating small clause normal forms
Andreas Nonnengart, Georg Rock and Christoph Weidenbach
412-426
Rank/activity: A canonical form for binary resolution
J. D. Horton and Bruce Spencer
427-441
Towards efficient subsumption
Tanel Tammet
Back matter