Automated Deduction - CADE-14 (Record no. 187908)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 05356nam a22005655i 4500 |
| 001 - CONTROL NUMBER | |
| control field | 978-3-540-69140-2 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | DE-He213 |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20240423132442.0 |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr nn 008mamaa |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 121227s1997 gw | s |||| 0|eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9783540691402 |
| -- | 978-3-540-69140-2 |
| 024 7# - OTHER STANDARD IDENTIFIER | |
| Standard number or code | 10.1007/3-540-63104-6 |
| Source of number or code | doi |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | Q334-342 |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | TA347.A78 |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | UYQ |
| Source | bicssc |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM004000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | UYQ |
| Source | thema |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 006.3 |
| Edition number | 23 |
| 245 10 - TITLE STATEMENT | |
| Title | Automated Deduction - CADE-14 |
| Medium | [electronic resource] : |
| Remainder of title | 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 - 17, 1997, Proceedings / |
| Statement of responsibility, etc | edited by William McCune. |
| 250 ## - EDITION STATEMENT | |
| Edition statement | 1st ed. 1997. |
| 264 #1 - | |
| -- | Berlin, Heidelberg : |
| -- | Springer Berlin Heidelberg : |
| -- | Imprint: Springer, |
| -- | 1997. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | XV, 469 p. |
| Other physical details | online resource. |
| 336 ## - | |
| -- | text |
| -- | txt |
| -- | rdacontent |
| 337 ## - | |
| -- | computer |
| -- | c |
| -- | rdamedia |
| 338 ## - | |
| -- | online resource |
| -- | cr |
| -- | rdacarrier |
| 347 ## - | |
| -- | text file |
| -- | |
| -- | rda |
| 490 1# - SERIES STATEMENT | |
| Series statement | Lecture Notes in Artificial Intelligence, |
| International Standard Serial Number | 2945-9141 ; |
| Volume number/sequential designation | 1249 |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc | 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 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Artificial intelligence. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer systems. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Machine theory. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Artificial Intelligence. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer System Implementation. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Formal Languages and Automata Theory. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | McCune, William. |
| Relator term | editor. |
| Relator code | edt |
| -- | http://id.loc.gov/vocabulary/relators/edt |
| 710 2# - ADDED ENTRY--CORPORATE NAME | |
| Corporate name or jurisdiction name as entry element | SpringerLink (Online service) |
| 773 0# - HOST ITEM ENTRY | |
| Title | Springer Nature eBook |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Display text | Printed edition: |
| International Standard Book Number | 9783540631040 |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Display text | Printed edition: |
| International Standard Book Number | 9783662179680 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE | |
| Uniform title | Lecture Notes in Artificial Intelligence, |
| -- | 2945-9141 ; |
| Volume number/sequential designation | 1249 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | <a href="https://doi.org/10.1007/3-540-63104-6">https://doi.org/10.1007/3-540-63104-6</a> |
| 912 ## - | |
| -- | ZDB-2-SCS |
| 912 ## - | |
| -- | ZDB-2-SXCS |
| 912 ## - | |
| -- | ZDB-2-LNC |
| 912 ## - | |
| -- | ZDB-2-BAE |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Koha item type | eBooks-CSE-Springer |
No items available.