000 06877cam a2200877 i 4500
001 ocn150397185
003 OCoLC
005 20250703143520.0
006 m o d
007 cr |||||||||||
008 060821s1998 gw a ob 001 0 eng d
010 _z 98028492
040 _aNLGGC
_beng
_epn
_cNLGGC
_dVT2
_dOCLCO
_dYNG
_dCSU
_dAU@
_dDKDLA
_dHDC
_dGW5XE
_dOCLCA
_dOCLCQ
_dOCLCF
_dUA@
_dNUI
_dOCL
_dOCLCO
_dOCLCQ
_dOCLCO
_dOCLCQ
_dUAB
_dESU
_dOCLCQ
_dBUF
_dKIJ
_dOCLCQ
_dOCLCA
_dWYU
_dCANPU
_dOL$
_dOCLCQ
_dLEAUB
_dOCLCQ
_dEUX
_dOCLCQ
_dOCLCO
_dOCLCQ
_dWSU
_dOCLCO
_dCOA
_dOCLCQ
015 _aGB9852368
_2bnb
016 7 _a007757488
_2Uk
019 _a436629221
_a644324603
_a769770640
_a793077752
_a993770293
_a1006403729
_a1009235854
_a1012878094
_a1014447719
_a1020031233
_a1027296784
_a1036749109
_a1038421330
_a1038491040
_a1039516083
_a1039684102
_a1066585467
_a1078835398
_a1081246124
_a1086530052
_a1162705952
_a1238295098
_a1340082486
020 _a9783540691105
_q(electronic bk.)
020 _a3540691103
_q(electronic bk.)
020 _z3540646752
020 _z9783540646754
024 7 _a10.1007/BFb0054239
_2doi
024 8 _a(WaSeSS)ssj0000321524
029 0 _aNLGGC
_b296864188
029 1 _aAU@
_b000044634994
029 1 _aAU@
_b000051316232
029 1 _aAU@
_b000051702351
029 1 _aAU@
_b000058011729
029 1 _aAU@
_b000058157525
029 1 _aNZ1
_b14997142
029 1 _aNZ1
_b15296931
029 1 _aAU@
_b000074442870
029 1 _aAU@
_b000060467660
035 _a(OCoLC)150397185
_z(OCoLC)436629221
_z(OCoLC)644324603
_z(OCoLC)769770640
_z(OCoLC)793077752
_z(OCoLC)993770293
_z(OCoLC)1006403729
_z(OCoLC)1009235854
_z(OCoLC)1012878094
_z(OCoLC)1014447719
_z(OCoLC)1020031233
_z(OCoLC)1027296784
_z(OCoLC)1036749109
_z(OCoLC)1038421330
_z(OCoLC)1038491040
_z(OCoLC)1039516083
_z(OCoLC)1039684102
_z(OCoLC)1066585467
_z(OCoLC)1078835398
_z(OCoLC)1081246124
_z(OCoLC)1086530052
_z(OCoLC)1162705952
_z(OCoLC)1238295098
_z(OCoLC)1340082486
050 4 _aQA76.9.A96
072 7 _aUYQ
_2bicssc
072 7 _aTJFM1
_2bicssc
072 7 _aCOM004000
_2bisacsh
072 7 _aUYQ
_2thema
082 0 4 _a006.3/33
084 _a54.72
_2bcl
049 _aMAIN
245 0 0 _aAutomated deduction, CADE-15 :
_b15th International conference on automated deduction, Lindau, Germany, July 5-10, 1998 : proceedings.
246 3 _aAutomated deduction
246 3 _aCADE-15
260 _aBerlin :
_bSpringer,
_c©1998.
300 _a1 online resource (xiv, 441 pages) :
_billustrations
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
347 _bPDF
490 1 _aLecture notes in artificial intelligence
504 _aIncludes bibliographical references and index.
520 _aThis book constitutes the refereed proceedings of the 15th International Conference on Automated Deduction, CADE-15, held in Lindau, Germany, in July 1998. The volume presents three invited contributions together with 25 revised full papers and 10 revised system descriptions; these were selected from a total of 120 submissions. The papers address all current issues in automated deduction and theorem proving based on resolution, superposition, model generation and elimination, or connection tableau calculus, in first-order, higher-order, intuitionistic, or modal logics, and describe applications to geometry, computer algebra, or reactive systems.
505 0 _aReasoning about deductions in linear logic -- A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia -- Proving geometric theorems using clifford algebra and rewrite rules -- System description: similarity-based lemma generation for model elimination -- System description: Verification of distributed Erlang programs -- System description: Cooperation in model elimination: CPTHEO -- System description: CardTAP: The first theorem prover on a smart card -- System description: leanK 2.0 -- Extensional higher-order resolution -- X.R.S: Explicit reduction systems -- A first-order calculus for higher-order calculi -- About the confluence of equational pattern rewrite systems -- Unification in lambda-calculi with if-then-else -- System description: An equational constraints solver -- System description: CRIL platform for SAT -- System description: Proof planning in higher-order logic with?Clam -- System description: An interface between CLAM and HOL -- System description: Leo -- A higher-order theorem prover -- Superposition for divisible torsion-free abelian groups -- Strict basic superposition -- Elimination of equality via transformation with ordering constraints -- A resolution decision procedure for the guarded fragment -- Combining Hilbert style and semantic reasoning in a resolution framework -- ACL2 support for verification projects -- A fast algorithm for uniform semi-unification -- Termination analysis by inductive evaluation -- Admissibility of fixpoint induction over partial types -- Automated theorem proving in a simple meta-logic for LF -- Deductive vs. model-theoretic approaches to formal verification -- Automated deduction of finite-state control programs for reactive systems -- A proof environment for the development of group communication systems -- On the relationship between non-horn magic sets and relevancy testing -- Certified version of Buchberger's algorithm -- Selectively instantiating definitions -- Using matings for pruning connection tableaux -- On generating small clause normal forms -- Rank/activity: A canonical form for binary resolution -- Towards efficient subsumption.
650 0 _aAutomatic theorem proving
_vCongresses.
_914919
650 0 _aLogic, Symbolic and mathematical
_vCongresses.
650 6 _aThéorèmes
_xDémonstration automatique
_vCongrès.
_914921
650 6 _aLogique symbolique et mathématique
_vCongrès.
650 7 _aAutomatic theorem proving
_2fast
_914923
650 7 _aLogic, Symbolic and mathematical
_2fast
_91341
650 1 7 _aAutomatische bewijsvoering.
_2gtt
_914926
655 7 _aproceedings (reports)
_2aat
655 7 _aConference papers and proceedings
_2fast
_96065
655 7 _aCongressen (vorm)
_2gtt
_98970
655 7 _aConference papers and proceedings.
_2lcgft
_96065
655 7 _aActes de congrès.
_2rvmgf
_9609890
700 1 _aKirchner, Claude.
_4edt
_920938
711 2 _aInternational Conference on Automated Deduction, CADE
_n(15th :
_d05-07-1998 - 10-07-1998 :
_cLindau, Germany)
_9925186
776 0 8 _iPrint version:
_tAutomated deduction, CADE-15
_w(NL-LeOCL)171392337
_w(OCoLC)39380406
830 0 _aLecture notes in computer science ;
_v1421.
_x1611-3349
830 0 _aLecture notes in computer science.
_pLecture notes in artificial intelligence.
_914916
856 4 0 _uhttps://link.springer.com/10.1007/BFb0054239
936 _aBATCHLOAD
994 _a92
_bATIST
999 _c636121
_d636121