Automated deduction : CADE-14 : 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 17, 1997 : proceedings
This book constitutes the strictly refereed proceedings of the 14th International Conference on Automated Deduction, CADE-14, held in Townsville, North Queensland, Australia, in July 1997. The volume presents 25 revised full papers selected from a total of 87 submissions; also included are 17 system...
שמור ב:
| מחבר ראשי: | |
|---|---|
| מחבר תאגידי: | |
| פורמט: | Livre numérique |
| שפה: | Anglais |
| יצא לאור: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| סדרה: | Lecture notes in computer science. Lecture notes in artificial intelligence
1249 |
| נושאים: | |
| גישה מקוונת: | 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-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, proceedings, William McCune (Ed.), 1997, Berlin, Springer, 1 vol. (XIV-462 p.), Lecture notes in computer science, 3-540-63104-6 • Automated Deduction - CADE-14, Texte imprimé, 9783662179680 |
| LEADER | 05870nam a22004097a 4500 | ||
|---|---|---|---|
| 001 | 969836 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155180312 | ||
| 020 | |a 9783540691402 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 006.333 | ||
| 082 | |a 004 | ||
| 100 | 1 | |a McCune, William Walker, |d 1953- | |
| 245 | 1 | 0 | |a Automated deduction : |b CADE-14 : 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 17, 1997 : proceedings |c [edited by] William McCune. |
| 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 1249 |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 The char-set method and its applications to automated reasoning -- Decidable call by need computations in term rewriting (extended abstract) -- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method -- On equality up-to constraints over finite trees, context unification, and one-step rewriting -- Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses -- The Clause-Diffusion theorem prover Peers-mcd (system description) -- Integration of automated and interactive theorem proving in ILF -- ILF-SETHEO -- SETHEO goes software engineering: Application of ATP to software reuse -- Proving System Correctness with KIV 3.0 -- A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry -- Automatic verification of cryptographic protocols with SETHEO -- A practical integration of first-order reasoning and decision procedures -- Some pitfalls of LK-to-LJ translations and how to avoid them -- Deciding intuitionistic propositional logic via translation into classical logic -- Lemma matching for a PTTP-based top-down theorem prover -- Exact knowledge compilation in predicate calculus: The partial achievement case -- Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving -- Alternating automata: Unifying truth and validity checking for temporal logics -- Connection-based proof construction in linear logic -- Resource-distribution via Boolean constraints -- Constructing a normal form for Property Theory -- ?mega: Towards a mathematical assistant -- Plagiator A learning prover -- CODE: A powerful prover for problems of condensed detachment -- A new method for testing decision procedures in modal logics -- Minlog: A minimal logictheorem prover -- SATO: An efficient prepositional prover -- Using a generalisation critic to find bisimulations for coinductive proofs -- A colored version of the ?-calculus -- A practical implementation of simple consequence relations using inductive definitions -- Soft typing for ordered resolution -- A classification of non-liftable orders for resolution -- Hybrid interactive theorem proving using nuprl and HOL -- Proof tactics for a theory of state machines in a graphical environment -- RALL: Machine-supported proofs for relation algebra -- Nuprl-Light: An implementation framework for higher-order logics -- XIsabelle: A system description -- XBarnacle: Making theorem provers more accessible -- The tableau browser SNARKS -- Jape: A calculator for animating proof-on-paper -- Evolving combinators -- Partial matching for analogy discovery in proofs and counter-examples -- Dialog. | |
| 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 strictly refereed proceedings of the 14th International Conference on Automated Deduction, CADE-14, held in Townsville, North Queensland, Australia, in July 1997. The volume presents 25 revised full papers selected from a total of 87 submissions; also included are 17 system descriptions and two invited contributions. The papers cover a wide range of current issues in the area including resolution, term rewriting, unification theory, induction, high-order logics, nonstandard logics, AI methods, and applications to software verification, geometry, and social science. | ||
| 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 | ||
| 711 | 2 | |a International conference on automated deduction |n (14 |d :1997 |c :Townsville, Australie). |4 aut | |
| 776 | 0 | |0 030726166 |t Automated deduction CADE-14 |o 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997 |o proceedings |f William McCune (Ed.) |d 1997 |c Berlin |n Springer |p 1 vol. (XIV-462 p.) |s Lecture notes in computer science |z 3-540-63104-6 | |
| 776 | 0 | |t Automated Deduction - CADE-14 |b Texte imprimé |z 9783662179680 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-63104-6 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-2P3FZQ2D-V |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:750669713 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-63104-6 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:754018687 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-63104-6 |z Accès INSA CVL | |
| 997 | |0 969836 |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/ | ||