Automated deduction in geometry : (Record no. 381830)

000 -LEADER
fixed length control field 05851cam a2200937Ka 4500
001 - CONTROL NUMBER
control field ocn761692861
003 - CONTROL NUMBER IDENTIFIER
control field OCoLC
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20200626111921.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 cnu---unuuu
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 111121s2011 gw ob 101 0 eng d
040 ## - CATALOGING SOURCE
Original cataloging agency GW5XE
Language of cataloging eng
Description conventions pn
Transcribing agency GW5XE
Modifying agency COO
-- UKMGB
-- OCLCQ
-- OCLCA
-- OCLCF
-- BEDGE
-- VT2
-- OCLCO
-- YDXCP
-- OCL
-- OCLCO
-- OCLCQ
-- VGM
-- ESU
-- OCLCQ
-- IOG
-- BUF
-- SHS
-- CEF
-- OCLCQ
-- U3W
-- AU@
-- OCLCA
-- WYU
-- YOU
-- LEAUB
-- W2U
-- OCLCQ
-- HS0
016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER
Record control number 015975100
Source Uk
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783642250705
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 364225070X
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Canceled/invalid ISBN 9783642250699
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.1007/978-3-642-25070-5
Source of number or code doi
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000048715132
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000058157381
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000060029297
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000060505258
029 1# - (OCLC)
OCLC library identifier DKDLA
System control number 820120-katalog:000687098
029 1# - (OCLC)
OCLC library identifier NLGGC
System control number 384338038
029 1# - (OCLC)
OCLC library identifier NZ1
System control number 14154157
035 ## - SYSTEM CONTROL NUMBER
System control number (OCoLC)761692861
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA448.D38
Item number I58 2011
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 516.00285
Edition number 23
049 ## - LOCAL HOLDINGS (OCLC)
Holding library MAIN
111 2# - MAIN ENTRY--MEETING NAME
Meeting name or jurisdiction name as entry element International Workshop on Automated Deduction in Geometry
Number of part/section/meeting (8th :
Date of meeting 2010 :
Location of meeting Munich, Germany)
9 (RLIN) 43420
245 10 - TITLE STATEMENT
Title Automated deduction in geometry :
Remainder of title 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, revised selected papers /
Statement of responsibility, etc. Pascal Schreck, Julien Narboux, Jürgen Richter-Gebert (eds.).
246 3# - VARYING FORM OF TITLE
Title proper/short title ADG 2010
260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Place of publication, distribution, etc. Berlin ;
-- New York :
Name of publisher, distributor, etc. Springer,
Date of publication, distribution, etc. ©2011.
300 ## - PHYSICAL DESCRIPTION
Extent 1 online resource (x, 258 pages)
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
Encoding format PDF
Source rda
490 1# - SERIES STATEMENT
Series statement Lecture notes in artificial intelligence ;
Volume/sequential designation 6877
490 1# - SERIES STATEMENT
Series statement Lecture notes in computer science,
International Standard Serial Number 0302-9743
490 1# - SERIES STATEMENT
Series statement LNCS sublibrary. SL 7, Artificial intelligence
490 ## - SERIES STATEMENT
Series statement Serienbezeichnung
504 ## - BIBLIOGRAPHY, ETC. NOTE
Bibliography, etc Includes bibliographical references and author index.
520 ## - SUMMARY, ETC.
Summary, etc. This book constitutes the thoroughly refereed post-workshop proceedings of the 8th International Workshop on Automated Deduction in Geometry, ADG 2010, held in Munich, Germany in July 2010. The 13 revised full papers presented were carefully selected during two rounds of reviewing and improvement from the lectures given at the workshop. Topics addressed by the papers are incidence geometry using some kind of combinatoric argument; computer algebra; software implementation; as well as logic and proof assistants.
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Cancellation patterns in automatic geometric theorem proving / Susanne Apel and Jürgen Richter-Gebert -- Exploring the foundations of discrete analytical geometry in Isabelle/HOL / Jacques Fleuriot -- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry / Laurent Fuchs and Laurent Théry -- Automatic calculation of plane loci using Gröbner bases and integration into a dynamic geometry system / Michael Gerhäuser and Alfred Wassermann -- Proof documents for automated origami theorem proving / Fadoua Ghourabi, Tetsuo Ida, and Asem Kasem -- The midpoint locus of a triangle in a corner / Daniel Lichtblau -- Some Lemmas to hopefully enable search methods to find short -- and human readable proofs for incidence theorems of projective geometry / Dominique Michelucci -- What is a line? / Dominique Michelucci -- On one method of proving inequalities in automated way / Pavel Pech -- Thousands of geometric problems for geometric theorem provers -- (TGTP) / Pedro Quaresma -- An investigation of Hilbert's implicit reasoning through proof -- discovery in idle-time / Phil Scott and Jacques Fleuriot -- A coherent logic based geometry theorem prover capable of -- producing formal and readable proofs / Sana Stojanović, Vesna Pavlović, and Predrag Janičić -- Automated generation of readable proofs for constructive geometry -- statements with the mass point method / Yu Zou and Jingzhong Zhang.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Geometry
General subdivision Data processing
Form subdivision Congresses.
9 (RLIN) 15943
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 #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 Geometry
General subdivision Data processing.
Source of heading or term fast
Authority record control number (OCoLC)fst00940870
9 (RLIN) 5492
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Mechanical Engineering.
Source of heading or term hilcc
9 (RLIN) 1897
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Mathematics.
Source of heading or term hilcc
9 (RLIN) 43421
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Engineering & Applied Sciences.
Source of heading or term hilcc
9 (RLIN) 9023
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Physical Sciences & Mathematics.
Source of heading or term hilcc
9 (RLIN) 11926
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer Science.
Source of heading or term hilcc
9 (RLIN) 941
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Mechanical Engineering - General.
Source of heading or term hilcc
9 (RLIN) 20039
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Geometry.
Source of heading or term hilcc
9 (RLIN) 2664
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Computer science
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Software engineering
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Computational complexity
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Artificial intelligence
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Computer graphics
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Artificial Intelligence (incl. Robotics)
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Mathematical Logic and Formal Languages
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Symbolic and Algebraic Manipulation
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Discrete Mathematics in Computer Science
655 #4 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Electronic books.
9 (RLIN) 396
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
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Schreck, Pascal.
9 (RLIN) 43422
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Narboux, Julien.
9 (RLIN) 43423
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Richter-Gebert, Jürgen,
Dates associated with a name 1963-
9 (RLIN) 21343
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Printed edition:
International Standard Book Number 9783642250699
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 ;
Volume number/sequential designation 6877.
9 (RLIN) 14916
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science.
9 (RLIN) 43424
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title LNCS sublibrary.
Number of part/section of a work SL 7,
Name of part/section of a work Artificial intelligence.
9 (RLIN) 20712
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://link-springer-com.libraryproxy.ist.ac.at/book/10.1007/978-3-642-25070-5">https://link-springer-com.libraryproxy.ist.ac.at/book/10.1007/978-3-642-25070-5</a>
938 ## -
-- YBP Library Services
-- YANK
-- 7274763
994 ## -
-- 92
-- ATIST
Holdings
Withdrawn status Lost status Damaged status Not for loan Collection code Permanent Location Current Location Date acquired Date last seen Price effective from Koha item type
  Not Lost     EBook e-Library e-Library 2020-06-26 2020-06-26 2020-06-26 eBook

Powered by Koha