8th International conference on automated deduction : Oxford, England, July 27 August 1, 1986 : proceedings
Tallennettuna:
| Yhteisötekijä: | |
|---|---|
| Muut tekijät: | |
| Aineistotyyppi: | Livre numérique |
| Kieli: | Anglais |
| Julkaistu: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Sarja: | Lecture notes in computer science
230 |
| Aiheet: | |
| Linkit: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Huomautus: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • 8th International conference on Automated deduction, Oxford, England, July 27-August 1, 1986, proceedings, Edited by Jörg H. Siekmann, Berlin, Springer, 1986, 1 vol. (IX-708 p.), Lecture notes in computer science, 3-540-16780-3 • 8th International Conference on Automated Deduction, Texte imprimé, 9783662198230 |
| LEADER | 06547nam a22003977a 4500 | ||
|---|---|---|---|
| 001 | 944998 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155210688 | ||
| 020 | |a 9783540398615 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 511.3 | ||
| 082 | |a 004 | ||
| 111 | 2 | |a International conference on automated deduction |n (8 |d :1986 |c :Oxford, Angleterre). | |
| 245 | 1 | 0 | |a 8th International conference on automated deduction : |b Oxford, England, July 27 August 1, 1986 : proceedings |c [edited by] Jörg H. Siekmann. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 230 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Connections and higher-order logic -- Commutation, transformation, and termination -- Full-commutation and fair-termination in equational (and combined) term-rewriting systems -- An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations -- Proving termination of associative commutative rewriting systems by rewriting -- Relating resolution and algebraic completion for Horn logic -- A simple non-termination test for the Knuth-Bendix method -- A new formula for the execution of categorical combinators -- Proof by induction using test sets -- How to prove equivalence of term rewriting systems without induction -- Sufficient completeness, term rewriting systems and anti-unification -- A new method for establishing refutational completeness in theorem proving -- A theory of diagnosis from first principles -- Some contributions to the logical analysis of circumscription -- Modal theorem proving -- Computational aspects of three-valued logic -- Resolution and quantified epistemic logics -- A commonsense theory of nonmonotonic reasoning -- Negative paramodulation -- The heuristics and experimental results of a new hyperparamodulation: HL-resolution -- ECR: An equality conditional resolution proof procedure -- Using narrowing to do isolation in symbolic equation solving an experiment in automated reasoning -- Formulation of induction formulas in verification of prolog programs -- Program verifier "Tatzelwurm": Reasoning about systems systems of linear inequalities -- An interactive verification system based on dynamic logic -- What you always wanted to know about clause graph resolution -- Parallel theorem proving with connection graphs -- Theory links in semantic graphs -- Abstraction usinggeneralization functions -- An improvement of deduction plans: Refutation plans -- Controlling deduction with proof condensation and heuristics -- Nested resolution -- Mechanizing constructive proofs -- Implementing number theory: An experiment with Nuprl -- Parallel algorithms for term matching -- Unification in combinations of collapse-free theories with disjoint sets of function symbols -- Combination of unification algorithms -- Unification in the data structure sets -- NP-completeness of the set unification and matching problems -- Matching with distributivity -- Unification in boolean rings -- Some relationships between unification, restricted unification, and matching -- A classification of many-sorted unification problems -- Unification in many-sorted equational theories -- Classes of first order formulas under various satisfiability definitions -- Diamond formulas in the dynamic logic of recursively enumerable programs -- A prolog machine -- A prolog technology theorem prover: Implementation by an extended prolog compiler -- Paths to high-performance automated theorem proving -- Purely functional implementation of a logic -- Causes for events: Their computation and applications -- How to clear a block: Plan formation in situational logic -- Deductive synthesis of sorting programs -- The TPS theorem proving system -- Trspec: A term rewriting based system for algebraic specifications -- Highly parallel inference machine -- Automatic theorem proving in the ISDV system -- The karlsruhe induction theorem proving system -- Overview of a theorem-prover for a computational logic -- GEO-prover A geometry theorem prover developed at UT -- The markgraf karl refutation procedure (MKRP) -- The J-machine: Functional programming with combinators -- The illinois prover: A general purpose resolutiontheorem prover -- Theorem proving systems of the Formel project -- The passau RAP system: Prototyping algebraic specifications using conditional narrowing -- RRL: A rewrite rule laboratory -- A geometry theorem prover based on Buchberger's algorithm -- REVE a rewrite rule laboratory -- ITP at argonne national laboratory -- Autologic at university of victoria -- Thinker -- The KLAUS automated deduction system -- The KRIPKE automated theorem proving system -- SHD-prover at university of texas at austin. | |
| 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 Siekmann, Jörg H., |d 1941- |4 pbd | |
| 776 | 0 | |0 030768179 |t 8th International conference on Automated deduction |o Oxford, England, July 27-August 1, 1986 |o proceedings |f Edited by Jörg H. Siekmann |c Berlin |n Springer |d 1986 |p 1 vol. (IX-708 p.) |s Lecture notes in computer science |z 3-540-16780-3 | |
| 776 | 0 | |t 8th International Conference on Automated Deduction |b Texte imprimé |z 9783662198230 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-16780-3 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-6V51J3FW-N |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:747914575 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-16780-3 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:750927283 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-16780-3 |z Accès INSA CVL | |
| 997 | |0 944998 |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/ | ||