Automated Deduction - CADE-15 de Claude Kirchner

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

Claude Kirchner

Helene Kirchner

en Limba Engleză Paperback – 24 iun 1998

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.

Citește tot Restrânge

Din seria Lecture Notes in Computer Science

20%

Preț: 1040^.03 lei
20%

Preț: 333^.46 lei
20%

Preț: 335^.08 lei
20%

Preț: 567^.60 lei
20%

Preț: 238^.01 lei
15%

Preț: 568^.74 lei
20%

Preț: 333^.46 lei
20%

Preț: 438^.69 lei
Preț: 373^.56 lei
20%

Preț: 336^.71 lei
20%

Preț: 148^.66 lei
20%

Preț: 310^.26 lei
20%

Preț: 632^.22 lei
20%

Preț: 747^.79 lei
20%

Preț: 1053^.45 lei
17%

Preț: 427^.22 lei
20%

Preț: 641^.78 lei
20%

Preț: 307^.71 lei
20%

Preț: 809^.19 lei
20%

Preț: 579^.56 lei
20%

Preț: 649^.49 lei
20%

Preț: 330^.23 lei
Preț: 389^.48 lei
20%

Preț: 607^.39 lei
20%

Preț: 538^.29 lei
20%

Preț: 1003^.66 lei
20%

Preț: 326^.98 lei
20%

Preț: 256^.27 lei
20%

Preț: 444^.17 lei
20%

Preț: 571^.63 lei
20%

Preț: 575^.48 lei
20%

Preț: 574^.05 lei
17%

Preț: 360^.19 lei
20%

Preț: 504^.57 lei
20%

Preț: 172^.69 lei
20%

Preț: 369^.12 lei
20%

Preț: 346^.40 lei
20%

Preț: 747^.79 lei
Preț: 402^.62 lei
20%

Preț: 584^.40 lei
20%

Preț: 569^.19 lei
20%

Preț: 1159^.14 lei
20%

Preț: 1386^.07 lei
20%

Preț: 343^.16 lei
20%

Preț: 309^.90 lei
20%

Preț: 122^.89 lei

Specificații

ISBN-13: 9783540646754
ISBN-10: 3540646752
Pagini: 464
Ilustrații: XIV, 450 p.
Dimensiuni: 155 x 235 x 24 mm
Greutate: 0.64 kg
Ediția:1998
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Lecture Notes in Artificial Intelligence

Locul publicării:Berlin, Heidelberg, Germany

Cuprins

Reasoning about deductions in linear logic.- A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia.- Proving geometric theorems using clifford algebra and rewrite rules.- System description: similarity-based lemma generation for model elimination.- System description: Verification of distributed Erlang programs.- System description: Cooperation in model elimination: CPTHEO.- System description: CardTAP: The first theorem prover on a smart card.- System description: leanK 2.0.- Extensional higher-order resolution.- X.R.S: Explicit reduction systems — A first-order calculus for higher-order calculi.- About the confluence of equational pattern rewrite systems.- Unification in lambda-calculi with if-then-else.- System description: An equational constraints solver.- System description: CRIL platform for SAT.- System description: Proof planning in higher-order logic with ?Clam.- System description: An interface between CLAM and HOL.- System description: Leo — A higher-order theorem prover.- Superposition for divisible torsion-free abelian groups.- Strict basic superposition.- Elimination of equality via transformation with ordering constraints.- A resolution decision procedure for the guarded fragment.- Combining Hilbert style and semantic reasoning in a resolution framework.- ACL2 support for verification projects.- A fast algorithm for uniform semi-unification.- Termination analysis by inductive evaluation.- Admissibility of fixpoint induction over partial types.- Automated theorem proving in a simple meta-logic for LF.- Deductive vs. model-theoretic approaches to formal verification.- Automated deduction of finite-state control programs for reactive systems.- A proof environment for the development of groupcommunication systems.- On the relationship between non-horn magic sets and relevancy testing.- Certified version of Buchberger's algorithm.- Selectively instantiating definitions.- Using matings for pruning connection tableaux.- On generating small clause normal forms.- Rank/activity: A canonical form for binary resolution.- Towards efficient subsumption.