Automated deduction, CADE-15 : (Record no. 636121)

MARC details
000 -LEADER
fixed length control field 06877cam a2200877 i 4500
001 - CONTROL NUMBER
control field ocn150397185
003 - CONTROL NUMBER IDENTIFIER
control field OCoLC
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20250703143520.0
006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS
fixed length control field m o d
007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION
fixed length control field cr |||||||||||
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 060821s1998 gw a ob 001 0 eng d
010 ## - LIBRARY OF CONGRESS CONTROL NUMBER
Canceled/invalid LC control number 98028492
040 ## - CATALOGING SOURCE
Original cataloging agency NLGGC
Language of cataloging eng
Description conventions pn
Transcribing agency NLGGC
Modifying agency VT2
-- OCLCO
-- YNG
-- CSU
-- AU@
-- DKDLA
-- HDC
-- GW5XE
-- OCLCA
-- OCLCQ
-- OCLCF
-- UA@
-- NUI
-- OCL
-- OCLCO
-- OCLCQ
-- OCLCO
-- OCLCQ
-- UAB
-- ESU
-- OCLCQ
-- BUF
-- KIJ
-- OCLCQ
-- OCLCA
-- WYU
-- CANPU
-- OL$
-- OCLCQ
-- LEAUB
-- OCLCQ
-- EUX
-- OCLCQ
-- OCLCO
-- OCLCQ
-- WSU
-- OCLCO
-- COA
-- OCLCQ
015 ## - NATIONAL BIBLIOGRAPHY NUMBER
National bibliography number GB9852368
Source bnb
016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER
Record control number 007757488
Source Uk
019 ## -
-- 436629221
-- 644324603
-- 769770640
-- 793077752
-- 993770293
-- 1006403729
-- 1009235854
-- 1012878094
-- 1014447719
-- 1020031233
-- 1027296784
-- 1036749109
-- 1038421330
-- 1038491040
-- 1039516083
-- 1039684102
-- 1066585467
-- 1078835398
-- 1081246124
-- 1086530052
-- 1162705952
-- 1238295098
-- 1340082486
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783540691105
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 3540691103
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Canceled/invalid ISBN 3540646752
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Canceled/invalid ISBN 9783540646754
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.1007/BFb0054239
Source of number or code doi
024 8# - OTHER STANDARD IDENTIFIER
Standard number or code (WaSeSS)ssj0000321524
029 0# - (OCLC)
OCLC library identifier NLGGC
System control number 296864188
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000044634994
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000051316232
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000051702351
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000058011729
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000058157525
029 1# - (OCLC)
OCLC library identifier NZ1
System control number 14997142
029 1# - (OCLC)
OCLC library identifier NZ1
System control number 15296931
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000074442870
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000060467660
035 ## - SYSTEM CONTROL NUMBER
System control number (OCoLC)150397185
Canceled/invalid control number (OCoLC)436629221
-- (OCoLC)644324603
-- (OCoLC)769770640
-- (OCoLC)793077752
-- (OCoLC)993770293
-- (OCoLC)1006403729
-- (OCoLC)1009235854
-- (OCoLC)1012878094
-- (OCoLC)1014447719
-- (OCoLC)1020031233
-- (OCoLC)1027296784
-- (OCoLC)1036749109
-- (OCoLC)1038421330
-- (OCoLC)1038491040
-- (OCoLC)1039516083
-- (OCoLC)1039684102
-- (OCoLC)1066585467
-- (OCoLC)1078835398
-- (OCoLC)1081246124
-- (OCoLC)1086530052
-- (OCoLC)1162705952
-- (OCoLC)1238295098
-- (OCoLC)1340082486
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA76.9.A96
072 #7 - SUBJECT CATEGORY CODE
Subject category code UYQ
Source bicssc
072 #7 - SUBJECT CATEGORY CODE
Subject category code TJFM1
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/33
084 ## - OTHER CLASSIFICATION NUMBER
Classification number 54.72
Number source bcl
049 ## - LOCAL HOLDINGS (OCLC)
Holding library MAIN
245 00 - TITLE STATEMENT
Title Automated deduction, CADE-15 :
Remainder of title 15th International conference on automated deduction, Lindau, Germany, July 5-10, 1998 : proceedings.
246 3# - VARYING FORM OF TITLE
Title proper/short title Automated deduction
246 3# - VARYING FORM OF TITLE
Title proper/short title CADE-15
260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Place of publication, distribution, etc. Berlin :
Name of publisher, distributor, etc. Springer,
Date of publication, distribution, etc. ©1998.
300 ## - PHYSICAL DESCRIPTION
Extent 1 online resource (xiv, 441 pages) :
Other physical details illustrations
336 ## - CONTENT TYPE
Content type term text
Content type code txt
Source rdacontent
337 ## - MEDIA TYPE
Media type term computer
Media type code c
Source rdamedia
338 ## - CARRIER TYPE
Carrier type term online resource
Carrier type code cr
Source rdacarrier
347 ## - DIGITAL FILE CHARACTERISTICS
File type text file
347 ## - DIGITAL FILE CHARACTERISTICS
Encoding format PDF
490 1# - SERIES STATEMENT
Series statement Lecture notes in artificial intelligence
504 ## - BIBLIOGRAPHY, ETC. NOTE
Bibliography, etc Includes bibliographical references and index.
520 ## - SUMMARY, ETC.
Summary, etc. This book constitutes the refereed proceedings of the 15th International Conference on Automated Deduction, CADE-15, held in Lindau, Germany, in July 1998. The volume presents three invited contributions together with 25 revised full papers and 10 revised system descriptions; these were selected from a total of 120 submissions. The papers address all current issues in automated deduction and theorem proving based on resolution, superposition, model generation and elimination, or connection tableau calculus, in first-order, higher-order, intuitionistic, or modal logics, and describe applications to geometry, computer algebra, or reactive systems.
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Reasoning about deductions in linear logic -- A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia -- Proving geometric theorems using clifford algebra and rewrite rules -- System description: similarity-based lemma generation for model elimination -- System description: Verification of distributed Erlang programs -- System description: Cooperation in model elimination: CPTHEO -- System description: CardTAP: The first theorem prover on a smart card -- System description: leanK 2.0 -- Extensional higher-order resolution -- X.R.S: Explicit reduction systems -- A first-order calculus for higher-order calculi -- About the confluence of equational pattern rewrite systems -- Unification in lambda-calculi with if-then-else -- System description: An equational constraints solver -- System description: CRIL platform for SAT -- System description: Proof planning in higher-order logic with?Clam -- System description: An interface between CLAM and HOL -- System description: Leo -- A higher-order theorem prover -- Superposition for divisible torsion-free abelian groups -- Strict basic superposition -- Elimination of equality via transformation with ordering constraints -- A resolution decision procedure for the guarded fragment -- Combining Hilbert style and semantic reasoning in a resolution framework -- ACL2 support for verification projects -- A fast algorithm for uniform semi-unification -- Termination analysis by inductive evaluation -- Admissibility of fixpoint induction over partial types -- Automated theorem proving in a simple meta-logic for LF -- Deductive vs. model-theoretic approaches to formal verification -- Automated deduction of finite-state control programs for reactive systems -- A proof environment for the development of group communication systems -- On the relationship between non-horn magic sets and relevancy testing -- Certified version of Buchberger's algorithm -- Selectively instantiating definitions -- Using matings for pruning connection tableaux -- On generating small clause normal forms -- Rank/activity: A canonical form for binary resolution -- Towards efficient subsumption.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Automatic theorem proving
Form subdivision Congresses.
9 (RLIN) 14919
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logic, Symbolic and mathematical
Form subdivision Congresses.
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Théorèmes
General subdivision Démonstration automatique
Form subdivision Congrès.
9 (RLIN) 14921
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logique symbolique et mathématique
Form subdivision Congrès.
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Automatic theorem proving
Source of heading or term fast
9 (RLIN) 14923
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logic, Symbolic and mathematical
Source of heading or term fast
9 (RLIN) 1341
650 17 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Automatische bewijsvoering.
Source of heading or term gtt
9 (RLIN) 14926
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term proceedings (reports)
Source of term aat
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Conference papers and proceedings
Source of term fast
9 (RLIN) 6065
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Congressen (vorm)
Source of term gtt
9 (RLIN) 8970
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Conference papers and proceedings.
Source of term lcgft
9 (RLIN) 6065
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Actes de congrès.
Source of term rvmgf
9 (RLIN) 609890
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Kirchner, Claude.
Relator code edt
9 (RLIN) 20938
711 2# - ADDED ENTRY--MEETING NAME
Meeting name or jurisdiction name as entry element International Conference on Automated Deduction, CADE
Number of part/section/meeting (15th :
Date of meeting 05-07-1998 - 10-07-1998 :
Location of meeting Lindau, Germany)
9 (RLIN) 925186
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Print version:
Title Automated deduction, CADE-15
Record control number (NL-LeOCL)171392337
-- (OCoLC)39380406
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science ;
Volume number/sequential designation 1421.
International Standard Serial Number 1611-3349
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science.
Name of part/section of a work Lecture notes in artificial intelligence.
9 (RLIN) 14916
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://link.springer.com/10.1007/BFb0054239">https://link.springer.com/10.1007/BFb0054239</a>
936 ## - OCLC/CONSER MISCELLANEOUS DATA (OCLC); PIECE USED FOR CATALOGING (pre-AACR2) (RLIN)
OCLC control number(s) of parallel record(s) (OCLC); Piece used for cataloging, PUC (RLIN) BATCHLOAD
994 ## -
-- 92
-- ATIST
Holdings
Withdrawn status Lost status Damaged status Not for loan Collection code Home library Current library Date acquired Total Checkouts Date last seen Price effective from Koha item type
  Not Lost     eBook LNCS e-Library e-Library 28/07/2022   28/07/2022 28/07/2022 eBook

Powered by Koha