7th international conference on automated deduction : Napa, California, USA May 14 16, 1984 : proceedings
The Seventh International Conference on Automated Deduction was held May 14-16, 19S4, in Napa, California. The conference is the primary forum for reporting research in all aspects of automated deduction, including the design, implementation, and applications of theorem-proving systems, knowledge re...
Αποθηκεύτηκε σε:
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | |
| Μορφή: | Livre numérique |
| Γλώσσα: | Anglais |
| Έκδοση: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Σειρά: | Lecture notes in computer science
170 |
| Θέματα: | |
| Διαθέσιμο 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: | • 7th international conference on Automated deduction, proceedings, Napa, California, May 14-16, 1984, Edited by R.E. Shostak, Berlin, Springer, 1984, 1 vol. (vi-508 p.), Lecture notes in computer science, 3-540-96022-8 • 7th International Conference on Automated Deduction, Texte imprimé, 9781475789249 |
| LEADER | 05600nam a22003977a 4500 | ||
|---|---|---|---|
| 001 | 972624 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155227254 | ||
| 020 | |a 9780387347684 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 511.3 | ||
| 082 | |a 510 | ||
| 111 | 2 | |a International conference on automated deduction |n (07 |d :1984 |c :Napa, Californie, Etats-Unis). | |
| 245 | 1 | 0 | |a 7th international conference on automated deduction : |b Napa, California, USA May 14 16, 1984 : proceedings |c [edited by] R. E. Shostak. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 170 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Universal Unification -- A Portable Environment for Research in Automated Reasoning -- A Natural Proof System Based on Rewriting Techniques -- EKL A Mathematically Oriented Proof Checker -- A Linear Characterization of NP-Complete Problems -- A Satisfiability Tester for Non-Clausal Propositional Calculus -- A Decision Method for Linear Temporal Logic -- A Progress Report on New Decision Algorithms for Finitely Presented Abelian Groups -- Canonical Forms in Finitely Presented Algebras -- Term Rewriting Systems and Algebra -- Termination of a Set of Rules Modulo a Set of Equations -- Associative-Commutative Unification -- A Linear Time Algorithm for a Subcase of Second Order Instantiation -- A New Equational Unification Method: A Generalisation of Martelli-Montanari s Algorithm -- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x 3 = x Implies Ring Commutativity -- A Narrowing Procedure for Theories with Constructors -- A General Inductive Completion Algorithm and Application to Abstract Data Types -- The Next Generation of Interactive Theorem Provers -- The Linked Inference Principle, II: The User s Viewpoint -- A New Interpretation of the Resolution Principle -- Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving -- Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs -- Analytic and Non-analytic Proofs -- Applications of Protected Circumscription -- Implementation Strategies for Plan-Based Deduction -- A Programming Notation for Tactical Reasoning -- The Mechanization of Existence Proofs of Recursive Predicates -- Solving Word Problems in Free Algebras Using Complexity Functions -- Solving a Problem in Relevance Logic with an Automated Theorem Prover. | |
| 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 The Seventh International Conference on Automated Deduction was held May 14-16, 19S4, in Napa, California. The conference is the primary forum for reporting research in all aspects of automated deduction, including the design, implementation, and applications of theorem-proving systems, knowledge representation and retrieval, program verification, logic programming, formal specification, program synthesis, and related areas. The presented papers include 27 selected by the program committee, an invited keynote address by Jorg Siekmann, and an invited banquet address by Patrick Suppes. Contributions were presented by authors from Canada, France, Spain, the United Kingdom , the United States, and West Germany. The first conference in this series was held a decade earlier in Argonne, Illinois. Following the Argonne conference were meetings in Oberwolfach, West Germany (1976), Cambridge, Massachusetts (1977), Austin, Texas (1979), Les Arcs, France (19S0), and New York, New York (19S2). Program Committee P. Andrews (CMU) W.W. Bledsoe (U. Texas) past chairman L. Henschen (Northwestern) G. Huet (INRIA) D. Loveland (Duke) past chairman R. Milner (Edinburgh) R. Overbeek (Argonne) T. Pietrzykowski (Acadia) D. Plaisted (U. Illinois) V. Pratt (Stanford) R. Shostak (SRI) chairman J. Siekmann (U. Kaiserslautern) R. Waldinger (SRI) Local Arrangements R. Schwartz (SRI) iv CONTENTS Monday Morning Universal Unification (Keynote Address) Jorg H. Siekmann (FRG) . | ||
| 650 | |a Logique symbolique et mathématique | ||
| 650 | |a Théorèmes |x Démonstration automatique | ||
| 650 | |a Mathématiques | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Shostak, Robert E. |4 pbd | |
| 776 | 0 | |0 025771701 |t 7th international conference on Automated deduction |o proceedings |o Napa, California, May 14-16, 1984 |f Edited by R.E. Shostak |c Berlin |n Springer |d 1984 |p 1 vol. (vi-508 p.) |s Lecture notes in computer science |z 3-540-96022-8 | |
| 776 | 0 | |t 7th International Conference on Automated Deduction |b Texte imprimé |z 9781475789249 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/978-0-387-34768-4 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-CP9NVXHW-K |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:750634626 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/978-0-387-34768-4 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:753990903 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/978-0-387-34768-4 |z Accès INSA CVL | |
| 997 | |0 972624 |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/ | ||