Automated Deduction - CADE-15: 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 15th International Conference on Automated Deduction, CADE-15, held in Lindau, Germany, in July 1998. The volume presents three invited contributions together with 25 revised full papers and 10 revised system descriptions; these were selected from a total of 120 submissions. The papers address all current issues in automated deduction and theorem proving based on resolution, superposition, model generation and elimination, or connection tableau calculus, in first-order, higher-order, intuitionistic, or modal logics, and describe applications to geometry, computer algebra, or reactive systems. 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

This book constitutes the refereed proceedings of the 15th International Conference on Automated Deduction, CADE-15, held in Lindau, Germany, in July 1998.
The volume presents three invited contributions together with 25 revised full papers and 10 revised system descriptions; these were selected from a total of 120 submissions. The papers address all current issues in automated deduction and theorem proving based on resolution, superposition, model generation and elimination, or connection tableau calculus, in first-order, higher-order, intuitionistic, or modal logics, and describe applications to geometry, computer algebra, or reactive systems.