Automated deduction : CADE-12 : 12th International Conference on Automated Deduction, Nancy, France, June 26-July 1, 1994 : proceedings
This volume contains the reviewed papers presented at the 12th International Conference on Automated Deduction (CADE-12) held at Nancy, France in June/July 1994. The 67 papers presented were selected from 177 submissions and document many of the most important research results in automated deduction...
Gardado en:
| Autor Principal: | |
|---|---|
| Autor Corporativo: | |
| 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
814 |
| 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-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, proceedings, Alan Bundy (Ed.), Berlin, Springer-Verlag, 1994, 1 vol. (XVI-848 p.), Lecture notes in computer science, 3-540-58156-1 • Automated Deduction CADE-12, Texte imprimé, 9783662170083 |
| LEADER | 07205nam a22004097a 4500 | ||
|---|---|---|---|
| 001 | 971969 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155216198 | ||
| 020 | |a 9783540484677 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 006.33 | ||
| 082 | |a 004 | ||
| 100 | 1 | |a Bundy, Alan R., |d 1947- | |
| 245 | 1 | 0 | |a Automated deduction : |b CADE-12 : 12th International Conference on Automated Deduction, Nancy, France, June 26-July 1, 1994 : proceedings |c [edited by] Alan Bundy. |
| 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 814 |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 crisis in finite mathematics: Automated reasoning as cause and cure -- A divergence critic -- Synthesis of induction orderings for existence proofs -- Lazy generation of induction hypotheses -- The search efficiency of theorem proving strategies -- A method for building models automatically. Experiments with an extension of OTTER -- Model elimination without contrapositives -- Induction using term orderings -- Mechanizable inductive proofs for a class of ? ? formulas -- On the connection between narrowing and proof by consistency -- A fixedpoint approach to implementing (Co)inductive definitions -- On notions of inductive validity for first-order equational clauses -- A new application for explanation-based generalisation within automated deduction -- Semantically guided first-order theorem proving using hyper-linking -- The applicability of logic program analysis and transformation to theorem proving -- Detecting non-provable goals -- A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we? -- The TPTP problem library -- Combination techniques for non-disjoint equational theories -- Primal grammars and unification modulo a binary clause -- Conservative query normalization on parallel circumscription -- Bottom-up evaluation of Datalog programs with arithmetic constraints -- On intuitionistic query answering in description bases -- Deductive composition of astronomical software from subroutine libraries -- Proof script pragmatics in IMPS -- A mechanization of strong Kleene logic for partial functions -- Algebraic factoring and geometry theorem proving -- Mechanically proving geometry theorems using a combination of Wu's method and Collins' method -- Str?ve and integers -- What is a proof? -- Termination, geometry and invariants -- Ordered chaining for totalorderings -- Simple termination revisited -- Termination orderings for rippling -- A novel asynchronous parallelism scheme for first-order logic -- Proving with BDDs and control of information -- Extended path-indexing -- Exporting and reflecting abstract metamathematics -- Associative-commutative deduction with constraints -- AC-superposition with constraints: No AC-unifiers needed -- The complexity of counting problems in equational matching -- Representing proof transformations for program optimization -- Exploring abstract algebra in constructive type theory -- Tactic theorem proving with refinement-tree proofs and metavariables -- Unification in an extensional lambda calculus with ordered function sorts and constant overloading -- Decidable higher-order unification problems -- Theory and practice of minimal modular higher-order E-unification -- A refined version of general E-unification -- A completion-based method for mixed universal and rigid E-unification -- On pot, pans and pudding or how to discover generalised critical Pairs -- Semantic tableaux with ordering restrictions -- Strongly analytic tableaux for normal modal logics -- Reconstructing proofs at the assertion level -- Problems on the generation of finite models -- Combining symbolic computation and theorem proving: Some problems of Ramanujan -- SCOTT: Semantically constrained otter system description -- Protein: A PROver with a Theory Extension INterface -- DELTA A bottom-up preprocessor for top-down theorem provers -- SETHEO V3.2: Recent developments -- KoMeT -- ?-MKRP: A proof development environment -- LeanT A P: Lean tableau-based theorem proving -- FINDER: Finite domain enumerator system description -- Symlog automated advice in Fitch-style proof construction -- KEIM: A toolkit for automated deduction -- Elf: Ameta-language for deductive systems -- EUODHILOS-II on top of GNU epoch -- Pi: An interactive derivation editor for the calculus of partial inductive definitions -- Mollusc a general proof-development shell for sequent-based logics -- KITP-93: An automated inference system for program analysis -- SPIKE: A system for sufficient completeness and parameterized inductive proofs -- Distributed theorem proving by Peers. | |
| 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 volume contains the reviewed papers presented at the 12th International Conference on Automated Deduction (CADE-12) held at Nancy, France in June/July 1994. The 67 papers presented were selected from 177 submissions and document many of the most important research results in automated deduction since CADE-11 was held in June 1992. The volume is organized in chapters on heuristics, resolution systems, induction, controlling resolutions, ATP problems, unification, LP applications, special-purpose provers, rewrite rule termination, ATP efficiency, AC unification, higher-order theorem proving, natural systems, problem sets, and system descriptions. | ||
| 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 (12 |d :1994 |c :Nancy, France). |4 aut | |
| 776 | 0 | |0 01911642X |t Automated deduction CADE-12 |o 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994 |o proceedings |f Alan Bundy (Ed.) |c Berlin |n Springer-Verlag |d 1994 |p 1 vol. (XVI-848 p.) |s Lecture notes in computer science |z 3-540-58156-1 | |
| 776 | 0 | |t Automated Deduction CADE-12 |b Texte imprimé |z 9783662170083 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-58156-1 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-Q760HC7M-4 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:750646667 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-58156-1 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:753997541 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-58156-1 |z Accès INSA CVL | |
| 997 | |0 971969 |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/ | ||