Automated deduction - CADE-16 : 16th International Conference on Automated Deduction Trento, Italy, July 7 10, 1999 : proceedings
Gardado en:
| Autor Corporativo: | |
|---|---|
| Outros autores: | |
| Formato: | Livre numérique |
| Idioma: | Anglais |
| Publicado: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Series: | Lecture notes in computer science. Lecture notes in artificial intelligence
1632 |
| Sujets: | |
| Acceso en liña: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
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 16, 16th International; Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings, [edited by] Harald Ganzinger, 1999, New York, Springer, 1 vol. (XIV-428 p.), Lecture notes in computer science, 3-540-66222-7 • Automated Deduction - CADE-16, Texte imprimé, 9783662182055 |
| LEADER | 05229nam a22003977a 4500 | ||
|---|---|---|---|
| 001 | 948623 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155176625 | ||
| 020 | |a 9783540486602 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 006.33 | ||
| 082 | |a 004 | ||
| 111 | 2 | |a International Conference on Automated Deduction |n (16 |d :1999 |c :Trente, Italie). | |
| 245 | 1 | 0 | |a Automated deduction - CADE-16 : |b 16th International Conference on Automated Deduction Trento, Italy, July 7 10, 1999 : proceedings |c [edited by] Harald Ganzinger. |
| 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 1632 |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 Session 1 -- A Dynamic Programming Approach to Categorial Deduction -- Tractable Transformations from Modal Provability Logics into First-Order Logic -- Session 2 -- Decision Procedures for Guarded Logics -- A PSpace Algorithm for Graded Modal Logic -- Session 3 -- Solvability of Context Equations with Two Context Variables Is Decidable -- Complexity of the Higher Order Matching -- Solving Equational Problems Efficiently -- Session 4 -- VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up -- A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers -- Presenting Proofs in a Human-Oriented Way -- Session 5 -- On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results -- Maslov s Class K Revisited -- Prefixed Resolution: A Resolution Method for Modal and Description Logics -- Session 6: System Descriptions -- System Description: Twelf A Meta-Logical Framework for Deductive Systems -- System Description: inka 5.0 - A Logic Voyager -- System Description: CutRes 0.1: Cut Elimination by Resolution -- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving -- System Description Using OBDD s for the Validationof Skolem Verification Conditions -- Fault-Tolerant Distributed Theorem Proving -- System Description: Waldmeister Improvements in Performance and Ease of Use -- Session 7 -- Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems -- A Formalization of Static Analyses in System F -- On Explicit Reflection in Theorem Proving and Formal Verification -- Session 8: System Descriptions -- System Description: Kimba, A Model Generator for Many-Valued First-Order Logics -- System Description:Teyjus A Compiler and Abstract Machine Based Implementation of ?Prolog -- Vampire -- System Abstract: E 0.3 -- Session 9 -- Invited Talk: Rewrite-Based Deduction and Symbolic Constraints -- Towards an Automatic Analysis of Security Protocols in First-Order Logic -- Session 10 -- A Confluent Connection Calculus -- Abstraction-Based Relevancy Testing for Model Elimination -- A Breadth-First Strategy for Mating Search -- Session 11: System Competitions -- The Design of the CADE-16 Inductive Theorem Prover Contest -- Session 12: System Descriptions -- System Description: Spass Version 1.0.0 -- K : A Theorem Prover for K -- System Description: CYNTHIA -- System Description: MCS: Model-Based Conjecture Searching -- Session 13 -- Embedding Programming Languages in Theorem Provers -- Extensional Higher-Order Paramodulation and RUE-Resolution -- Automatic Generation of Proof Search Strategies for Second-Order Logic. | |
| 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 | ||
| 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 Ganzinger, Harald, |d 1950-2004. |4 pbd | |
| 776 | 0 | |0 046268332 |t Automated deduction, CADE 16 |o 16th International; Conference on Automated Deduction, Trento, Italy, July 7-10, 1999 |o proceedings |f [edited by] Harald Ganzinger |d 1999 |c New York |n Springer |p 1 vol. (XIV-428 p.) |s Lecture notes in computer science |z 3-540-66222-7 | |
| 776 | 0 | |t Automated Deduction - CADE-16 |b Texte imprimé |z 9783662182055 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-48660-7 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-JXTFJ32J-3 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:748059067 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-48660-7 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:751510564 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-48660-7 |z Accès INSA CVL | |
| 997 | |0 948623 |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/ | ||