Automated deduction - CADE-17 : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 : proceedings
For the past 25 years the CADE conference has been the major forum for the presentation of new results in automated deduction. This volume contains the papers and system descriptions selected for the 17th International Conference on Automated Deduction, CADE-17, held June 17-20, 2000,at Carnegie Mel...
Αποθηκεύτηκε σε:
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | |
| Μορφή: | Livre numérique |
| Γλώσσα: | Anglais |
| Έκδοση: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Σειρά: | Lecture notes in computer science. Lecture notes in artificial intelligence
1831 |
| Θέματα: | |
| Διαθέσιμο 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 |
| Σημείωση: |
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-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 2000, proceedings, David McAllester (ed.), Berlin, Springer, 2000, 1 volume, Lecture notes in computer science, 3-540-67664-3 • Automated Deduction - CADE-17, Texte imprimé, 9783662176870 |
| LEADER | 06795nam a22003977a 4500 | ||
|---|---|---|---|
| 001 | 972164 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155219391 | ||
| 020 | |a 9783540451013 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 111 | 2 | |a International conference on automated deduction |n (17 |d :2000 |c :Pittsburgh). | |
| 245 | 1 | 0 | |a Automated deduction - CADE-17 : |b 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 : proceedings |c [edited by] David McAllester. |
| 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 1831 |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 Invited Talk: -- High-Level Verification Using Theorem Proving and Formalized Mathematics -- Session 1: -- Machine Instruction Syntax and Semantics in Higher Order Logic -- Proof Generation in the Touchstone Theorem Prover -- Wellfounded Schematic Definitions -- Session 2: -- Abstract Congruence Closure and Specializations -- A Framework for Cooperating Decision Procedures -- Modular Reasoning in Isabelle -- An Infrastructure for Intertheory Reasoning -- Session 3: -- Gödel s Algorithm for Class Formation -- Automated Proof Construction in Type Theory Using Resolution -- System Description: TPS: A Theorem Proving System for Type Theory -- The Nuprl Open Logical Environment -- System Description: aRa An Automatic Theorem Prover for Relation Algebras -- Invited Talk: -- Scalable Knowledge Representation and Reasoning Systems -- Session 4: -- Efficient Minimal Model Generation Using Branching Lemmas -- FDPLL A First-Order Davis-Putnam-Logeman-Loveland Procedure -- Rigid E-Unification Revisited -- Invited Talk: -- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice -- Session 5: -- Reducing Model Checking of the Many to the Few -- Simulation Based Minimization -- Rewriting for Cryptographic Protocol Verification -- System Description: *sat: A Platform for the Development of Modal Decision Procedures -- System Description: DLP -- Two Techniques to Improve Finite Model Search -- Session 6: -- Eliminating Dummy Elimination -- Extending Decision Procedures with Induction Schemes -- Complete Monotonic Semantic Path Orderings -- Session 7: -- Stratified Resolution -- Support Ordered Resolution -- System Description: IVY -- System Description: SystemOnTPTP -- System Description: PTTP+GLiDeS Semantically Guided PTTP -- Session 8: -- A Formalization of a Concurrent ObjectCalculus up to ?-Conversion -- A Resolution Decision Procedure for Fluted Logic -- ZRes: The Old Davis Putnam Procedure Meets ZBDD -- System Description: MBase, an Open Mathematical Knowledge Base -- System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level -- Session 9: -- On Unification for Bounded Distributive Lattices -- Reasoning with Individuals for the Description Logic -- System Description: Embedding Verification into Microsoft Excel -- System Description: Interactive Proof Critics in XBarnacle -- Tutorials: -- Tutorial: Meta-logical Frameworks -- Tutorial: Automated Deduction and Natural Language Understanding -- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic -- Workshops: -- Workshop: Model Computation Principles, Algorithms, Applications -- Workshop: Automation of Proof by Mathematical Induction -- Workshop: Type-Theoretic Languages: Proof-Search and Semantics -- Workshop: Automated Deduction in Education -- Workshop: The Role of Automated Deduction in Mathematics. | |
| 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 For the past 25 years the CADE conference has been the major forum for the presentation of new results in automated deduction. This volume contains the papers and system descriptions selected for the 17th International Conference on Automated Deduction, CADE-17, held June 17-20, 2000,at Carnegie Mellon University, Pittsburgh, Pennsylvania (USA). Fifty-three research papers and twenty system descriptions were submitted by researchers from ?fteen countries. Each submission was reviewed by at least three reviewers. Twenty-four research papers and ?fteen system descriptions were accepted. The accepted papers cover a variety of topics related to t- orem proving and its applications such as proof carrying code, cryptographic protocol veri?cation, model checking, cooperating decision procedures, program veri?cation, and resolution theorem proving. The program also included three invited lectures: High-level veri?cation using theorem proving and formalized mathematics by John Harrison, Sc- able Knowledge Representation and Reasoning Systems by Henry Kautz, and Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice by Carl Seger. Abstracts or full papers of these talks are included in this volume.In addition to the accepted papers, system descriptions, andinvited talks, this volumecontains one page summaries of four tutorials and ?ve workshops held in conjunction with CADE-17. | ||
| 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 McAllester, David, |d 1956- |4 pbd | |
| 776 | 0 | |0 051915553 |t Automated deduction - CADE-17 |o 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 2000 |o proceedings |f David McAllester (ed.) |c Berlin |n Springer |d 2000 |p 1 volume |s Lecture notes in computer science |z 3-540-67664-3 | |
| 776 | 0 | |t Automated Deduction - CADE-17 |b Texte imprimé |z 9783662176870 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/10721959 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-02KZ7JC8-H |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:75060056X |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/10721959 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:753961210 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/10721959 |z Accès INSA CVL | |
| 997 | |0 972164 |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/ | ||