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.
Author(s): Frank Pfenning (auth.), Claude Kirchner, Hélène Kirchner (eds.)
Series: Lecture Notes in Computer Science 1421 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1998
Language: English
Pages: 450
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs
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
