MARC details
| 000 -LEADER |
|---|
| fixed length control field |
09581cam a2201093 i 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
ocn150398533 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20250703143541.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 |
060821s1992 gw a ob 100 0 eng d |
| 010 ## - LIBRARY OF CONGRESS CONTROL NUMBER |
|---|
| Canceled/invalid LC control number |
92021886 |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
NLGGC |
| Language of cataloging |
eng |
| Description conventions |
pn |
| Transcribing agency |
NLGGC |
| Modifying agency |
CUSER |
| -- |
KIJ |
| -- |
OCLCO |
| -- |
GW5XE |
| -- |
OCLCA |
| -- |
ITD |
| -- |
OCLCF |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
UAB |
| -- |
ESU |
| -- |
OCLCQ |
| -- |
VT2 |
| -- |
CEF |
| -- |
DEHBZ |
| -- |
OCLCQ |
| -- |
OCLCA |
| -- |
UWO |
| -- |
YOU |
| -- |
OCLCQ |
| -- |
OCLCE |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
OCL |
| -- |
OCLCO |
| -- |
CAUOI |
| -- |
COA |
| -- |
OCLCL |
| -- |
OCLCQ |
| -- |
OCLCA |
| 019 ## - |
|---|
| -- |
321334074 |
| -- |
827358007 |
| -- |
1056391200 |
| -- |
1063893863 |
| -- |
1067177727 |
| -- |
1081200651 |
| -- |
1153025700 |
| -- |
1288405833 |
| -- |
1320925839 |
| -- |
1340073549 |
| -- |
1416630451 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783540472797 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3540472797 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
038755727X |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
9780387557274 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
354055727X |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
9783540557272 |
| 024 8# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
(WaSeSS)ssj0000324517 |
| 029 0# - (OCLC) |
|---|
| OCLC library identifier |
NLGGC |
| System control number |
296873527 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
NZ1 |
| System control number |
15296957 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)150398533 |
| Canceled/invalid control number |
(OCoLC)321334074 |
| -- |
(OCoLC)827358007 |
| -- |
(OCoLC)1056391200 |
| -- |
(OCoLC)1063893863 |
| -- |
(OCoLC)1067177727 |
| -- |
(OCoLC)1081200651 |
| -- |
(OCoLC)1153025700 |
| -- |
(OCoLC)1288405833 |
| -- |
(OCoLC)1320925839 |
| -- |
(OCoLC)1340073549 |
| -- |
(OCoLC)1416630451 |
| 042 ## - AUTHENTICATION CODE |
|---|
| Authentication code |
dlr |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.63 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
006.3 |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
54.10 |
| Number source |
bcl |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
SS 4800 |
| Number source |
rvk |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
ST 285 |
| Number source |
rvk |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
7,41 |
| Number source |
ssgn |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
DAT 706f |
| Number source |
stub |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
DAT 716f |
| Number source |
stub |
| 049 ## - LOCAL HOLDINGS (OCLC) |
|---|
| Holding library |
MAIN |
| 111 2# - MAIN ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
LPAR (Conference) |
| Number of part/section/meeting |
(3rd : |
| Date of meeting |
1992 : |
| Location of meeting |
Saint Petersburg, Russia) |
| 9 (RLIN) |
21091 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Logic programming and automated reasoning : |
| Remainder of title |
International Conference LPAR '92, St. Petersburg, Russia, July 15-20, 1992 : proceedings / |
| Statement of responsibility, etc. |
A. Voronkov (ed.). |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc. |
Berlin : |
| Name of publisher, distributor, etc. |
Springer-Verlag, |
| Date of publication, distribution, etc. |
©1992. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 online resource (XIV, 509 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 |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture notes in computer science ; |
| Volume/sequential designation |
624 |
| 500 ## - GENERAL NOTE |
|---|
| General note |
Conferentie voortzetting van: Russian Conference on Logic Programming. |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
This volume contains the proceedings of LPAR '92, the international conference on logic programming and automated reasoning held in St. Petersburg in July 1992. The aim of the conference was to bring together researchers from the Russian and the international logic programming and theorem proving communities. The topics of interest covered by papers inthe volume include automated theorem proving, non-monotonic reasoning, applications of mathematical logic to computer science, deductive databases, implementation of declarative concepts, and programming in non-classical logics. LPAR '92 is the successor of the First and Second Russian Conferences on Logic Programming held in 1990 and 1991, respectively, the proceedings of which were publishedin LNAI Vol. 592. |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
Soundness and completeness of partial deductions for well-founded semantics -- On deductive planning and the frame problem -- On resolution in fragments of classical linear logic (extended abstract) -- A procedure for automatic proof nets construction -- Free logic and infinite constraint networks -- Towards probabilistic knowledge bases -- Two-level grammar: A functional/logic query language for database and knowledge-base systems -- Extending deductive database languages by embedded implications -- Controlling redundancy in large search spaces: Argonne-style theorem proving through the years -- Resolution for many-valued logics -- An ordered theory resolution calculus -- Application of automated deduction to the search for single axioms for exponent groups -- Elementary lower bounds for the lengths of refutations -- Shortening proofs by quantifier introduction -- Reform compilation for nonlinear recursion -- Pruning infinite failure branches in programs with occur-check -- The use of planning critics in mechanizing inductive proofs --??-Calculus: An algorithmic interpretation of classical natural deduction -- Building proofs by analogy via the Curry-Howard Isomorphism -- On the use of the constructive omega-rule within automated deduction -- OR-parallel theorem proving with random competition -- Parallel computation of multiple sets-of-support -- Towards using the Andorra Kernel Language for industrial real-time applications -- Unification in a combination of equational theories with shared constants and its application to primal algebras -- Non-clausal resolution and superposition with selection and redundancy criteria -- Relating innermost, weak, uniform and modular termination of term rewriting systems -- A two steps semantics for logic programs with negation -- Generalized negation as failure and semantics of normal disjunctive logic programs -- General model theoretic semantics for Higher-Order horn logic programming -- Disjunctive deductive databases -- Netlog -- A concept oriented logic programming language -- From the past to the future: Executing temporal logic programs -- Computing induction axioms -- Consistency of equational enrichments -- A programming logic for a verified structured assembly language -- The unification of infinite sets of terms and its applications -- Unification in order-sorted type theory -- Infinite, canonical string rewriting systems generated by completion -- Spes: A system for logic program transformation -- Linear Objects: A logic framework for open system programming -- ISAR: An interactive system for algebraic implementation proofs -- Mathpert: Computer support for learning algebra, trig, and calculus -- MegaLog -- A platform for developing knowledge base management systems -- SPIKE, an automatic theorem prover -- An application to teaching in logic course of ATP based on natural deduction -- A generic logic environment -- ElipSys A parallel programming system based on logic -- Opium -- A high-level debugging environment -- An inductive theorem prover based on narrowing -- A cooperative answering system -- MIZ-PR: A theorem prover for polymorphic and recursive functions -- ProPre A programming language with proofs -- FRIENDLY-WAM: An interactive tool to understand the compilation of PROLOG -- SEPIA -- a Basis for Prolog extensions -- The external database in SICStus Prolog -- The KCM system: Speeding-up logic programming through hardware support -- Logician's Workbench -- EUODHILOS: A general reasoning system for a variety of logics -- The EKS-V1 system -- CHIP and Propia. |
| 506 ## - RESTRICTIONS ON ACCESS NOTE |
|---|
| Materials specified |
Use copy |
| Standardized terminology for access restriction |
Restrictions unspecified |
| Source of term |
star |
| Institution to which field applies |
MiAaHDL |
| 533 ## - REPRODUCTION NOTE |
|---|
| Type of reproduction |
Electronic reproduction. |
| Place of reproduction |
[Place of publication not identified]: |
| Agency responsible for reproduction |
HathiTrust Digital Library. |
| Date of reproduction |
2021. |
| Institution to which field applies |
MiAaHDL |
| 538 ## - SYSTEM DETAILS NOTE |
|---|
| System details note |
Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Library Federation, December 2002. |
| Uniform Resource Identifier |
<a href="http://purl.oclc.org/DLF/benchrepro0212">http://purl.oclc.org/DLF/benchrepro0212</a> |
| Institution to which field applies |
MiAaHDL |
| 583 1# - ACTION NOTE |
|---|
| Action |
digitized |
| Time/date of action |
2021. |
| Jurisdiction |
HathiTrust Digital Library |
| Status |
committed to preserve |
| Source of term |
pda |
| Institution to which field applies |
MiAaHDL |
| 611 27 - SUBJECT ADDED ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
Automation |
| Source of heading or term |
gnd |
| 9 (RLIN) |
837199 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer science. |
| 9 (RLIN) |
941 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Artificial intelligence. |
| 9 (RLIN) |
1340 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logic |
| General subdivision |
Symbolic and mathematical. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Electronic data processing. |
| 9 (RLIN) |
6665 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logic programming |
| General subdivision |
Congresses. |
| 9 (RLIN) |
966929 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Automatic theorem proving |
| General subdivision |
Congresses. |
| 9 (RLIN) |
966928 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Programmation logique |
| General subdivision |
Congrès. |
| 9 (RLIN) |
14822 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Théorèmes |
| General subdivision |
Démonstration automatique |
| -- |
Congrès. |
| 9 (RLIN) |
14928 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Informatique. |
| 9 (RLIN) |
14930 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Intelligence artificielle. |
| 9 (RLIN) |
15884 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
computer science. |
| Source of heading or term |
aat |
| 9 (RLIN) |
941 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
data processing. |
| Source of heading or term |
aat |
| 9 (RLIN) |
14620 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
artificial intelligence. |
| Source of heading or term |
aat |
| 9 (RLIN) |
1340 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logic programming |
| Source of heading or term |
fast |
| 9 (RLIN) |
6178 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Electronic data processing |
| Source of heading or term |
fast |
| 9 (RLIN) |
6665 |
| 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 |
Artificial intelligence |
| Source of heading or term |
fast |
| 9 (RLIN) |
1340 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer science |
| Source of heading or term |
fast |
| 9 (RLIN) |
941 |
| 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 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Automatisches Beweisverfahren |
| Source of heading or term |
gnd |
| 9 (RLIN) |
14924 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Künstliche Intelligenz |
| Source of heading or term |
gnd |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logik |
| Source of heading or term |
gnd |
| 9 (RLIN) |
20555 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logische Programmierung |
| Source of heading or term |
gnd |
| 9 (RLIN) |
19535 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Problemlösen |
| Source of heading or term |
gnd |
| 9 (RLIN) |
33079 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Kongress |
| Source of heading or term |
gnd |
| 9 (RLIN) |
8384 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Automation |
| Source of heading or term |
gnd |
| 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 |
| 650 17 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logisch programmeren. |
| Source of heading or term |
gtt |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Automatic theorem proving |
| Form subdivision |
Congresses. |
| Source of heading or term |
nli |
| 9 (RLIN) |
14919 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logic programming |
| Form subdivision |
Congresses. |
| Source of heading or term |
nli |
| 9 (RLIN) |
14819 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Programmation logique |
| General subdivision |
Congrès. |
| Source of heading or term |
ram |
| 9 (RLIN) |
14822 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Théorèmes |
| General subdivision |
Démonstration automatique. |
| Source of heading or term |
ram |
| 9 (RLIN) |
15071 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings |
| Source of term |
fast |
| 9 (RLIN) |
6065 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Voronkov, Andrei, |
| Dates associated with a name |
1959- |
| Relator code |
edt |
| 9 (RLIN) |
16227 |
| 711 2# - ADDED ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
International Conference on Logic Programming and Automated Reasoning, LPAR |
| Number of part/section/meeting |
(St. Petersburg, Russia : |
| Date of meeting |
1992) |
| 9 (RLIN) |
21093 |
| 758 ## - |
|---|
| -- |
has work: |
| -- |
Logic programming and automated reasoning (Text) |
| -- |
https://id.oclc.org/worldcat/entity/E39PCGB7q6jJBRj7ht6f37GMbm |
| -- |
https://id.oclc.org/worldcat/ontology/hasWork |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| Title |
Logic programming and automated reasoning |
| Record control number |
(NL-LeOCL)096095318 |
| -- |
(OCoLC)898889526 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture notes in computer science ; |
| Volume number/sequential designation |
624. |
| 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/BFb0013043">https://link.springer.com/10.1007/BFb0013043</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 |