000 04980nam a22005775i 4500
001 978-3-540-69110-5
003 DE-He213
005 20240423132533.0
007 cr nn 008mamaa
008 121227s1998 gw | s |||| 0|eng d
020 _a9783540691105
_9978-3-540-69110-5
024 7 _a10.1007/BFb0054239
_2doi
050 4 _aQ334-342
050 4 _aTA347.A78
072 7 _aUYQ
_2bicssc
072 7 _aCOM004000
_2bisacsh
072 7 _aUYQ
_2thema
082 0 4 _a006.3
_223
245 1 0 _aAutomated Deduction - CADE-15
_h[electronic resource] :
_b15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings /
_cedited by Claude Kirchner, Helene Kirchner.
250 _a1st ed. 1998.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c1998.
300 _aXIV, 450 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v1421
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 groupcommunication 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.
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.
650 0 _aArtificial intelligence.
650 0 _aMachine theory.
650 0 _aComputer science.
650 1 4 _aArtificial Intelligence.
650 2 4 _aFormal Languages and Automata Theory.
650 2 4 _aComputer Science Logic and Foundations of Programming.
700 1 _aKirchner, Claude.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aKirchner, Helene.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540646754
776 0 8 _iPrinted edition:
_z9783662196786
830 0 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v1421
856 4 0 _uhttps://doi.org/10.1007/BFb0054239
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
912 _aZDB-2-BAE
942 _cSPRINGER
999 _c188850
_d188850