MARC record from Internet Archive

LEADER: 05128cam 2200757 a 4500
001 ocm35029668
003 OCoLC
005 20201026074800.0
008 960627s1996 gw a b 101 0 eng
010 $a 96029057
040 $aDLC$beng$cDLC$dOCL$dC$Q$dBAKER$dNLGGC$dBTCTA$dLVB$dYDXCP$dOCLCG$dUAB$dZWZ$dGW5XE$dOCLCQ$dDEBSZ$dBDX$dMUU$dOCLCO$dOCLCF$dOCLCA$dOCLCQ$dOCLCO$dOCLCQ$dOCL$dOCLCO$dCAUOI$dOCLCQ$dCSJ$dOCLCQ$dOCLCA$dUWO$dHUELT$dTJC$dOCLCQ$dIEUOL
015 $a96,N29,0357$2dnb
016 7 $a947871500$2DE-101
019 $a960141797
020 $a3540615113$q(alk. paper)
020 $a9783540615118$q(alk. paper)
024 3 $a9783540615118
035 $a(OCoLC)35029668$z(OCoLC)960141797
050 00 $aQA76.9.A96$bI57 1996
082 00 $a006.3/3$220
084 $a54.72$2bcl
111 2 $aInternational Conference on Automated Deduction$n(13th :$d1996 :$cNew Brunswick, N.J.)
245 10 $aAutomated deduction, CADE-13 :$b13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996 : proceedings /$cM.A. McRobbie, J.K. Slaney, eds.
246 30 $aCADE-13
260 $aBerlin ;$aNew York :$bSpringer,$c©1996.
300 $axv, 764 pages :$billustrations ;$c24 cm
336 $atext$btxt$2rdacontent
337 $aunmediated$bn$2rdamedia
338 $avolume$bnc$2rdacarrier
490 1 $aLecture notes in computer science ;$v1104.$aLecture notes in artificial intelligence
504 $aIncludes bibliographical references and index.
530 $aAlso issued online.
505 0 $aSaturation-based theorem proving: Past successes and future potential / Harald Ganzinger -- A resolution theorem prover for intuitionistic logic / Tanel Tammet -- Proof-terms for classical and intuitionistic resolution / David Pym, Eike Ritter and Lincoln Wallen -- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-Unification / Andrei Voronkov -- Extensions to a generalization critic for inductive proof / Andrew Ireland and Alan Bundy -- Learning domain knowledge to improve theorem proving / Jorg Denzinger and Stephan Schulz -- Patching faulty conjectures / Martin Protzen -- Internal analogy in theorem proving / Erica Melis and Jon Whittle -- Termination of theorem proving by reuse / Thomas Kolbe and Christoph Walther -- Termination of algorithms over non-freely generated data types / Claus Sengler -- ABSFOL: a proof checker with abstraction / Fausto Giunchiglia and Adolfo Villafiorita.
520 $a"This book constitutes the refereed proceedings of the 13th International Conference on Automated Deduction, CADE-13, held in July/August 1996 in New Brunswick, NJ, USA, as part of FLoC '96. The volume presents 46 revised regular papers selected from a total of 114 submissions in this category; also included are 15 selected system descriptions and abstracts of two invited talks. The CADE conferences are the major forum for the presentation of new results in all aspects of automated deduction. Therefore, the volume is a timely report on the state-of-the-art in the area."--PUBLISHER'S WEBSITE.
506 $aInternet access restricted to Vanderbilt users.
650 0 $aAutomatic theorem proving$vCongresses.
650 0 $aLogic, Symbolic and mathematical$vCongresses.
650 1 $aLogic, Symbolic and mathematical.
650 6 $aLogique symbolique et mathématique$vCongrès.
650 6 $aThéorèmes$xDémonstration automatique$vCongrès.
650 7 $aAutomatic theorem proving.$2fast$0(OCoLC)fst00822777
650 7 $aLogic, Symbolic and mathematical.$2fast$0(OCoLC)fst01002068
650 17 $aAutomatische bewijsvoering.$2gtt
650 7 $aLogique symbolique et mathématique$xCongrès.$2ram
650 7 $aThéorèmes$xDémonstration automatique$xCongrès.$2ram
655 7 $aConference papers and proceedings.$2fast$0(OCoLC)fst01423772
700 1 $aMcRobbie, M. A.$q(Michael A.)
700 1 $aSlaney, J. K.$q(John K.)
830 0 $aLecture notes in computer science ;$v1104.
830 0 $aLecture notes in computer science.$pLecture notes in artificial intelligence.
856 41 $3SpringerLink$uhttps://doi.org/10.1007/3-540-61511-3
856 41 $uhttp://springerlink.metapress.com/openurl.asp?genre=issue&issn=0302-9743&volume=1104$zRestricted to SpringerLink subscribers
856 41 $uhttp://link.springer.com/10.1007/3-540-61511-3$zeBook available for UOIT via SpringerLink. Click link to access
856 4 $3Cover$uhttp://swbplus.bsz-bw.de/bsz053441044cov.htm$v20150910142355
856 4 $xLNCS$uhttp://www.springerlink.com/openurl.asp?genre=issue&issn=0302-9743&volume=1104$zConnect to Internet resource
938 $aBaker & Taylor$bBKTY$c121.00$d121.00$i3540615113$n0002885473$sactive
938 $aBrodart$bBROD$n50297422$c$113.00
938 $aBaker and Taylor$bBTCP$n96029057
938 $aYBP Library Services$bYANK$n1335744
029 1 $aAU@$b000012556998
029 1 $aDEBSZ$b053441044
029 1 $aNLGGC$b149718047
029 1 $aNZ1$b4723666
029 1 $aZWZ$b025839470
994 $aZ0$bP4A
948 $hNO HOLDINGS IN P4A - 193 OTHER HOLDINGS