MARC details
| 000 -LEADER |
|---|
| fixed length control field |
05190cam a2200685 a 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
ocn326712344 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20250703150419.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 unu---||||| |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
950613s1995 gw a ob 100 0 eng d |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
SCPER |
| Language of cataloging |
eng |
| Description conventions |
pn |
| Transcribing agency |
CUSER |
| Modifying agency |
OCLCQ |
| -- |
OCLCF |
| -- |
UV0 |
| -- |
GW5XE |
| -- |
ITD |
| -- |
OCLCO |
| -- |
NUI |
| -- |
OCL |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
UAB |
| -- |
ESU |
| -- |
VT2 |
| -- |
OCLCQ |
| -- |
OCLCA |
| -- |
OCLCQ |
| -- |
EUX |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCQ |
| 019 ## - |
|---|
| -- |
827358382 |
| -- |
858926445 |
| -- |
990472414 |
| -- |
1005785539 |
| -- |
1081205094 |
| -- |
1162696387 |
| -- |
1238333065 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783540492351 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3540492356 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3540593381 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783540593386 |
| 024 7# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.1007/3-540-59338-1 |
| Source of number or code |
doi |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
NZ1 |
| System control number |
14996670 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
NZ1 |
| System control number |
15315887 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)326712344 |
| Canceled/invalid control number |
(OCoLC)827358382 |
| -- |
(OCoLC)858926445 |
| -- |
(OCoLC)990472414 |
| -- |
(OCoLC)1005785539 |
| -- |
(OCoLC)1081205094 |
| -- |
(OCoLC)1162696387 |
| -- |
(OCoLC)1238333065 |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.9.A96 |
| Item number |
T33 1995 |
| 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 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
005.1/1 |
| Edition number |
20 |
| 049 ## - LOCAL HOLDINGS (OCLC) |
|---|
| Holding library |
MAIN |
| 111 2# - MAIN ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
TABLEAUX '95 |
| Date of meeting |
(1995 : |
| Location of meeting |
Sankt Goar, Germany) |
| 9 (RLIN) |
34236 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Theorem proving with analytic tableaux and related methods : |
| Remainder of title |
4th international workshop, TABLEAUX '95, Schloss Rheinfels, St. Goar, Germany, May 7-10, 1995 : proceedings / |
| Statement of responsibility, etc. |
Peter Baumgartner, Reiner Hähnle, Joachim Posegga, eds. |
| 246 30 - VARYING FORM OF TITLE |
|---|
| Title proper/short title |
TABLEAUX '95 |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc. |
Berlin ; |
| -- |
New York : |
| Name of publisher, distributor, etc. |
Springer, |
| Date of publication, distribution, etc. |
©1995. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 online resource (x, 352 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 |
918. |
| Series statement |
Lecture notes in artificial intelligence |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
This volume constitutes the proceedings of the 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, TABLEAU '95, held at Schlo Rheinfels, St. Goar, Germany in May 1995. Originally tableau calculi and their relatives were favored primarily as a pedagogical device because of their advantages at the presentation level. The 23 full revised papers in this book bear witness that these methods have now gained fundamental importance in theorem proving, particularly as competitors for resolution methods. The book is organized in sections on extensions, modal logic, intuitionistic logic, the connection method and model elimination, non-clausal proof procedures, linear logic, higher-order logic, and applications. |
| 588 0# - SOURCE OF DESCRIPTION NOTE |
|---|
| Source of description note |
Print version record. |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
Issues in theorem proving based on the connection method -- Rigid E-unification simplified -- Generating finite counter examples with semantic tableaux -- Semantic tableaus for inheritance nets -- Using connection method in modal logics: Some advantages -- Labelled tableaux for multi-modal logics -- Refutation systems for prepositional modal logics -- On transforming intuitionistic matrix proofs into standard-sequent proofs -- A connection based proof method for intuitionistic logic -- Tableau for intuitionistic predicate logic as metatheory -- Model building and interactive theory discovery -- Link deletion in model elimination -- Specifications of inference rules and their automatic translation -- Constraint model elimination and a PTTP-implementation -- Non-elementary speedups between different versions of tableaux -- Syntactic reduction of predicate tableaux to propositional tableaux -- Classical Lambek logic -- Linear logic with isabelle: Pruning the proof search tree -- Linear analytic tableaux -- Higher-order tableaux -- Propositional logics on the computer -- MacKE: Yet another proof assistant & automated pedagogic tool -- Using the theorem prover SETHEO for verifying the development of a communication protocol in FOCUS -A Case Study- |
| 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 |
Nonclassical mathematical logic |
| Form subdivision |
Congresses. |
| 9 (RLIN) |
34237 |
| 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 mathématique non classique |
| Form subdivision |
Congrès. |
| 9 (RLIN) |
40794 |
| 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 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Nonclassical mathematical logic |
| Source of heading or term |
fast |
| 9 (RLIN) |
23923 |
| 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 |
Baumgartner, Peter. |
| 9 (RLIN) |
31487 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Hähnle, Reiner. |
| 9 (RLIN) |
25349 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Posegga, Joachim. |
| 9 (RLIN) |
28896 |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| Main entry heading |
TABLEAUX '95 (1995 : Sankt Goar, Germany). |
| Title |
Theorem proving with analytic tableaux and related methods. |
| Place, publisher, and date of publication |
Berlin ; New York : Springer, ©1995 |
| International Standard Book Number |
3540593381 |
| Record control number |
(DLC) 95174471 |
| -- |
(OCoLC)32644245 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture notes in computer science ; |
| Volume number/sequential designation |
918. |
| 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/3-540-59338-1">https://link.springer.com/10.1007/3-540-59338-1</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 |