Automated deduction - CADE-15 : 15th International Conference on Automated Deduction Lindau, Germany, July 5 10, 1998 : proceedings
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 fro...
Zapisane w:
| Korporacja: | |
|---|---|
| Kolejni autorzy: | , |
| Format: | Livre numérique |
| Język: | Anglais |
| Wydane: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Seria: | Lecture notes in computer science. Lecture notes in artificial intelligence
1421 |
| Hasła przedmiotowe: | |
| Dostęp online: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Komentarz: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Automated deduction CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, proceedings, Claude Kirchner, Hélène Kirchner (Eds.), 1998, Berlin, Springer, 1 vol. (XIV-441 p.), Lecture notes in computer science, 3-540-64675-2 • Automated Deduction - CADE-15, Texte imprimé, 9783662196786 |
| LEADER | 05430nam a22004217a 4500 | ||
|---|---|---|---|
| 001 | 944158 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155177060 | ||
| 020 | |a 9783540691105 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 082 | |a 006.33 | ||
| 111 | 2 | |a International conference on automated deduction |n (15 |d :1998 |c :Lindau, Allemagne). | |
| 245 | 1 | 0 | |a Automated deduction - CADE-15 : |b 15th International Conference on Automated Deduction Lindau, Germany, July 5 10, 1998 : proceedings |c [edited by] Claude Kirchner, Hélène Kirchner. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science. Lecture notes in artificial intelligence |v 1421 |x 1611-3349 |x 2945-9141 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a 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. | |
| 506 | |a Accès en ligne pour les établissements français bénéficiaires des licences nationales | ||
| 506 | |a Accès soumis à abonnement pour tout autre établissement | ||
| 506 | |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 | ||
| 520 | |a 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. | ||
| 650 | |a Informatique | ||
| 650 | |a Intelligence artificielle | ||
| 650 | |a Logique symbolique et mathématique | ||
| 650 | |a Théorèmes |x Démonstration automatique | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Kirchner, Claude, |d 1951- |4 pbd | |
| 700 | 1 | |a Kirchner, Hélène, |d 1952-...., |c informaticienne. |4 pbd | |
| 776 | 0 | |0 035967773 |t Automated deduction CADE-15 |o 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998 |o proceedings |f Claude Kirchner, Hélène Kirchner (Eds.) |d 1998 |c Berlin |n Springer |p 1 vol. (XIV-441 p.) |s Lecture notes in computer science |z 3-540-64675-2 | |
| 776 | 0 | |t Automated Deduction - CADE-15 |b Texte imprimé |z 9783662196786 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/BFb0054239 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-C0VX0129-1 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:747893497 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/BFb0054239 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:750906510 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/BFb0054239 |z Accès INSA CVL | |
| 997 | |0 944158 |1 Livre numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||