Automated deduction : Cade-13 : 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996 : proceedings
This book constitutes the refereed proceedings of the 13th International Conference on Automated Deduction, CADE-13, held in July/August 1996 in New Brunswick, NJ, USA, as part of FLoC '96. The volume presents 46 revised regular papers selected from a total of 114 submissions in this category;...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Korporativní autor: | |
| Další autoři: | |
| Médium: | Livre numérique |
| Jazyk: | Anglais |
| Vydáno: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Edice: | Lecture notes in computer science. Lecture notes in artificial intelligence
1104 |
| Témata: | |
| On-line přístup: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Poznámka: |
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-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996, proceedings, M.A. McRobbie, J.K. Slaney, eds, 1996, Berlin, Springer, 1 vol. (XV-764 p.), Lecture notes in computer science, 3-540-61511-3 • Automated Deduction - Cade-13, Texte imprimé, 9783662176726 |
| LEADER | 06753nam a22004097a 4500 | ||
|---|---|---|---|
| 001 | 970621 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN15519366X | ||
| 020 | |a 9783540686873 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 100 | 1 | |a McRobbie, Michael A., |d 1950- | |
| 245 | 1 | 0 | |a Automated deduction : |b Cade-13 : 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996 : proceedings |c [edited by] M. A. McRobbie, J. K. Slaney. |
| 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 1104 |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 Saturation-based theorem proving: Past successes and future potential -- A resolution theorem prover for intuitionistic logic -- Proof-terms for classical and intuitionistic resolution -- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification -- Extensions to a generalization critic for inductive proof -- Learning domain knowledge to improve theorem proving -- Patching faulty conjectures -- Internal analogy in theorem proving -- Termination of theorem proving by reuse -- Termination of algorithms over non-freely generated data types -- ABSFOL: A proof checker with abstraction -- SPASS & FLOTTER version 0.42 -- The design of the CADE-13 ATP system competition -- SCAN Elimination of predicate quantifiers -- GEOTHER: A geometry theorem prover -- Structuring metatheory on inductive definitions -- An embedding of Ruby in Isabelle -- Mechanical verification of mutually recursive procedures -- FasTraC a decentralized traffic control system based on logic programming -- Presenting machine-found proofs -- MUltlog 1.0: Towards an expert system for many-valued logics -- CtCoq: A system presentation -- An introduction to geometry expert -- SiCoTHEO: Simple competitive parallel theorem provers -- What can we hope to achieve from automated deduction? -- Unification algorithms cannot be combined in polynomial time -- Unification and matching modulo nilpotence -- An improved lower bound for the elementary theories of trees -- INKA: The next generation -- XRay: A prolog technology theorem prover for default reasoning: A system description -- IMPS: An updated system description -- The tableau-based theorem prover 3 T A P Version 4.0 -- System description generating models by SEM -- Optimizing proof search in model elimination -- An abstract machine for fixed-order dynamicallystratified programs -- Unification in pseudo-linear sort theories is decidable -- Theorem proving with group presentations: Examples and questions -- Transforming termination by self-labelling -- Theorem proving in cancellative abelian monoids (extended abstract) -- On the practical value of different definitional translations to normal form -- Converting non-classical matrix proofs into sequent-style systems -- Efficient model generation through compilation -- Algebra and automated deduction -- On Shostak's decision procedure for combinations of theories -- Ground resolution with group computations on semantic symmetries -- A new method for knowledge compilation: The achievement by cycle search -- Rewrite semantics for production rule systems: Theory and applications -- Experiments in the heuristic use of past proof experience -- Lemma discovery in automating induction -- Advanced indexing operations on substitution trees -- Semantic trees revisited: Some new completeness results -- Building decision procedures for modal logics from propositional decision procedures The case study of modal K -- Resolution-based calculi for modal and temporal logics -- Tableaux and algorithms for Propositional Dynamic Logic with Converse -- Reflection of formal tactics in a deductive reflection framework -- Walther recursion -- Proof search with set variable instantiation in the Calculus of Constructions -- Search strategies for resolution in temporal logics -- Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices -- Grammar specification in categorial logics and theorem proving -- Path indexing for AC-theories -- More Church-Rosser proofs (in Isabelle/HOL) -- Partitioning methods for satisfiability testing on large formulas. | |
| 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 13th International Conference on Automated Deduction, CADE-13, held in July/August 1996 in New Brunswick, NJ, USA, as part of FLoC '96. The volume presents 46 revised regular papers selected from a total of 114 submissions in this category; also included are 15 selected system descriptions and abstracts of two invited talks. The CADE conferences are the major forum for the presentation of new results in all aspects of automated deduction. Therefore, the volume is a timely report on the state-of-the-art in the area. | ||
| 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 Slaney, John K. |4 pbd | |
| 711 | 2 | |a International Conference on Automated Deduction |n (13 |d :1996 |c :New Brunswick, N. J.). |4 aut | |
| 776 | 0 | |0 025839470 |t Automated deduction, CADE-13 |o 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996 |o proceedings |f M.A. McRobbie, J.K. Slaney, eds |d 1996 |c Berlin |n Springer |p 1 vol. (XV-764 p.) |s Lecture notes in computer science |z 3-540-61511-3 | |
| 776 | 0 | |t Automated Deduction - Cade-13 |b Texte imprimé |z 9783662176726 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-61511-3 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-RT097DSK-8 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:750661275 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-61511-3 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:754010848 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-61511-3 |z Accès INSA CVL | |
| 997 | |0 970621 |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/ | ||