MARC details
| 000 -LEADER |
|---|
| fixed length control field |
07383cam a2200805 a 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
ocn288565700 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20250703145813.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 cn||||||||| |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
081217s2008 gw a ob 101 0 eng d |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
GW5XE |
| Language of cataloging |
eng |
| Description conventions |
pn |
| Transcribing agency |
GW5XE |
| Modifying agency |
OCLCQ |
| -- |
OCLCA |
| -- |
OCLCF |
| -- |
BEDGE |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCL |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
NAM |
| -- |
OCLCA |
| -- |
OCLCQ |
| -- |
WURST |
| -- |
W2U |
| -- |
ERF |
| -- |
QE2 |
| -- |
COM |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
OCLCL |
| 019 ## - |
|---|
| -- |
1087000997 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783540710707 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3540710701 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783540710691 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3540710698 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
AU@ |
| System control number |
000048720792 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
NZ1 |
| System control number |
12798286 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)288565700 |
| Canceled/invalid control number |
(OCoLC)1087000997 |
| 037 ## - SOURCE OF ACQUISITION |
|---|
| Stock number |
978-3-540-71069-1 |
| Source of stock number/acquisition |
Springer |
| Note |
http://www.springerlink.com |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.9.A96 |
| Item number |
I38 2008eb |
| 055 #3 - CLASSIFICATION NUMBERS ASSIGNED IN CANADA |
|---|
| Classification number |
QA75 |
| Item number |
.L38 no.5195 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
006.3 |
| Edition number |
23 |
| 049 ## - LOCAL HOLDINGS (OCLC) |
|---|
| Holding library |
MAIN |
| 111 2# - MAIN ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
IJCAR (Conference) |
| Number of part/section/meeting |
(4th : |
| Date of meeting |
2008 : |
| Location of meeting |
Sydney, N.S.W.) |
| 9 (RLIN) |
31486 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Automated Reasoning : |
| Remainder of title |
fourth International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008 : proceedings / |
| Statement of responsibility, etc. |
Alessandro Armando, Peter Baumgartner, Gilles Dowek (eds.). |
| 246 30 - VARYING FORM OF TITLE |
|---|
| Title proper/short title |
IJCAR 2008 |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Name of publisher, distributor, etc. |
Berlin ; |
| Place of publication, distribution, etc. |
New York : |
| Name of publisher, distributor, etc. |
Springer, |
| Date of publication, distribution, etc. |
2008. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 online resource (xii, 556 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 |
5195. |
| Series statement |
Lecture notes in artificial intelligence |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references and index. |
| 588 0# - SOURCE OF DESCRIPTION NOTE |
|---|
| Source of description note |
Print version record. |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
Session 1: Invited Talk -- Software Verification: Roles and Challenges for Automatic Decision Procedures -- Session 2: Specific Theories -- Proving Bounds on Real-Valued Functions with Computations -- Linear Quantifier Elimination -- Quantitative Separation Logic and Programs with Lists -- On Automating the Calculus of Relations -- Session 3: Automated Verification -- Towards SMT Model Checking of Array-Based Systems -- Preservation of Proof Obligations from Java to the Java Virtual Machine -- Efficient Well-Definedness Checking -- Session 4: Protocol Verification -- Proving Group Protocols Secure Against Eavesdroppers -- Session 5: System Descriptions 1 -- Automated Implicit Computational Complexity Analysis (System Description) -- LogAnswer -- A Deduction-Based Question Answering System (System Description) -- A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description) -- The Abella Interactive Theorem Prover (System Description) -- LEO-II -- A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) -- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) -- The Complexity of Conjunctive Query Answering in Expressive Description Logics -- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments -- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse -- Session 8: Herbrand Award Ceremony -- Automata-Based Axiom Pinpointing -- Individual Reuse in Description Logic Reasoning -- The Logical Difference Problem for Description Logic Terminologies -- Session 10: System Descriptions 2 -- Aligator: A Mathematica Package for Invariant Generation (System Description) -- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) -- iProver -- An Instantiation-Based Theorem Prover for First-Order Logic (System Description) -- An Experimental Evaluation of Global Caching for (System Description) -- Multi-completion with Termination Tools (System Description) -- MTT: The Maude Termination Tool (System Description) -- Celf -- A Logical Framework for Deductive and Concurrent Systems (System Description) -- Canonicity! -- Unification and Matching Modulo Leaf-Permutative Equational Presentations -- Modularity of Confluence -- Automated Complexity Analysis Based on the Dependency Pair Method -- Canonical Inference for Implicational Systems -- Challenges in the Automated Verification of Security Protocols -- Session 14: Theorem Proving 1 -- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets -- Proof Systems for Effectively Propositional Logic -- MaLARea SG1 -- Machine Learner for Automated Reasoning with Semantic Guidance -- CASC-J4 The 4th IJCAR ATP System Competition -- Session 16: Theorem Proving 2 -- Labelled Splitting -- Engineering DPLL(T) + Saturation -- THF0 -- The Core of the TPTP Language for Higher-Order Logic -- Focusing in Linear Meta-logic -- Certifying a Tree Automata Completion Checker -- Automated Induction with Constrained Tree Automata. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
This book constitutes the refereed proceedings of the 4th International Joint Conference on Automated Reasoning, IJCAR 2008, held in Sydney, Australia, in August 2008. The 26 revised full research papers and 13 revised system descriptions presented together with 4 invited papers and a summary of the CASC-J4 systems competition were carefully reviewed and selected from 80 full paper and 17 system description submissions. The papers address the entire spectrum of research in automated reasoning and are organized in topical sections on specific theories, automated verification, protocol verification, system descriptions, modal logics, description logics, equational theories, theorem proving, CASC, the 4th IJCAR ATP system competition, logical frameworks, and tree automata. |
| 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 |
Computer logic |
| Form subdivision |
Congresses. |
| 9 (RLIN) |
15040 |
| 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 informatique |
| Form subdivision |
Congrès. |
| 9 (RLIN) |
26959 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Informatique. |
| Source of heading or term |
eclas |
| 9 (RLIN) |
14930 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Automatic theorem proving. |
| Source of heading or term |
fast |
| Authority record control number |
(OCoLC)fst00822777 |
| 9 (RLIN) |
14923 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer logic. |
| Source of heading or term |
fast |
| Authority record control number |
(OCoLC)fst00872265 |
| 9 (RLIN) |
6177 |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
wiskunde |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
mathematics |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
computerwetenschappen |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
computer sciences |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
kunstmatige intelligentie |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
artificial intelligence |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
logica |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
logic |
| 653 00 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
software engineering |
| 653 10 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Information and Communication Technology (General) |
| 653 10 - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
Informatie- en communicatietechnologie (algemeen) |
| 655 #2 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Congress |
| 9 (RLIN) |
11670 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings. |
| Source of term |
fast |
| Authority record control number |
(OCoLC)fst01423772 |
| 9 (RLIN) |
6065 |
| 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 |
Armando, Alessandro. |
| 9 (RLIN) |
16663 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Baumgartner, Peter. |
| 9 (RLIN) |
31487 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Dowek, Gilles. |
| 9 (RLIN) |
31488 |
| 758 ## - |
|---|
| -- |
has work: |
| -- |
Automated reasoning (Text) |
| -- |
https://id.oclc.org/worldcat/entity/E39PCFFKH6J7MgtX6txFGqqcMX |
| -- |
https://id.oclc.org/worldcat/ontology/hasWork |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| Main entry heading |
IJCAR 2008 (2008 : Sydney, Australia). |
| Title |
Automated Reasoning. |
| Place, publisher, and date of publication |
Berlin ; New York : Springer, 2008 |
| International Standard Book Number |
9783540710691 |
| -- |
3540710698 |
| Record control number |
(OCoLC)265034159 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture notes in computer science ; |
| Volume number/sequential designation |
5195. |
| 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/978-3-540-71070-7">https://link.springer.com/10.1007/978-3-540-71070-7</a> |
| 994 ## - |
|---|
| -- |
92 |
| -- |
ATIST |