Automated Deduction — CADE-15: 15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings

Reasoning about deductions in linear logic....Pages 1-2
A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia....Pages 3-16
Proving geometric theorems using clifford algebra and rewrite rules....Pages 17-32
System description: similarity-based lemma generation for model elimination....Pages 33-37
System description: Verification of distributed Erlang programs....Pages 38-41
System description: Cooperation in model elimination: CPTHEO....Pages 42-46
System description: CardT A P: The first theorem prover on a smart card....Pages 47-50
System description: leanK 2.0....Pages 51-55
Extensional higher-order resolution....Pages 56-71
X.R.S: Explicit reduction systems — A first-order calculus for higher-order calculi....Pages 72-87
About the confluence of equational pattern rewrite systems....Pages 88-102
Unification in lambda-calculi with if-then-else....Pages 103-118
System description: An equational constraints solver....Pages 119-123
System description: CRIL platform for SAT....Pages 124-128
System description: Proof planning in higher-order logic with λClam....Pages 129-133
System description: An interface between CL A M and HOL....Pages 134-138
System description: Leo — A higher-order theorem prover....Pages 139-143
Superposition for divisible torsion-free abelian groups....Pages 144-159
Strict basic superposition....Pages 160-174
Elimination of equality via transformation with ordering constraints....Pages 175-190
A resolution decision procedure for the guarded fragment....Pages 191-204
Combining Hilbert style and semantic reasoning in a resolution framework....Pages 205-219
ACL2 support for verification projects....Pages 220-238
A fast algorithm for uniform semi-unification....Pages 239-253
Termination analysis by inductive evaluation....Pages 254-269
Admissibility of fixpoint induction over partial types....Pages 270-285
Automated theorem proving in a simple meta-logic for LF....Pages 286-300
Deductive vs. model-theoretic approaches to formal verification....Pages 301-301
Automated deduction of finite-state control programs for reactive systems....Pages 302-316
A proof environment for the development of group communication systems....Pages 317-332
On the relationship between non-horn magic sets and relevancy testing....Pages 333-348
Certified version of Buchberger's algorithm....Pages 349-364
Selectively instantiating definitions....Pages 365-380
Using matings for pruning connection tableaux....Pages 381-396
On generating small clause normal forms....Pages 397-411
Rank/activity: A canonical form for binary resolution....Pages 412-426
Towards efficient subsumption....Pages 427-441