LEADER 03886nam  22006735  450 
001 996466091903316
005 20200701012452.0
010   $a3-540-48586-4
024 7 $a10.1007/BFb0030541
035   $a(CKB)1000000000234145
035   $a(SSID)ssj0000324193
035   $a(PQKBManifestationID)11236835
035   $a(PQKBTitleCode)TC0000324193
035   $a(PQKBWorkID)10304645
035   $a(PQKB)11704877
035   $a(DE-He213)978-3-540-48586-5
035   $a(PPN)155163639
035   $a(EXLCZ)991000000000234145
100   $a20121227d1994      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aIsabelle$b[electronic resource] $eA Generic Theorem Prover /$fby Lawrence C. Paulson
205   $a1st ed. 1994.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1994.
215   $a1 online resource (XIX, 329 p.) 
225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v828
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-58244-4 
327   $aFoundations -- Getting started with Isabelle -- Advanced methods -- Basic use of Isabelle -- Proof management: The subgoal module -- Tactics -- Tacticals -- Theorems and forward proof -- Theories, terms and types -- Defining logics -- Syntax transformations -- Substitution tactics -- Simplification -- The classical reasoner -- Basic concepts -- First-order logic -- Zermelo-Fraenkel set theory -- Higher-order logic -- First-order sequent calculus -- Constructive Type Theory -- Syntax of Isabelle Theories.
330   $aAs a generic theorem prover, Isabelle supports a variety of logics. Distinctive features include Isabelle's representation of logics within a meta-logic and the use of higher-order unification to combine inference rules. Isabelle can be applied to reasoning in pure mathematics or verification of computer systems. This volume constitutes the Isabelle documentation. It begins by outlining theoretical aspects and then demonstrates the use in practice. Virtually all Isabelle functions are described, with advice on correct usage and numerous examples. Isabelle's built-in logics are also described in detail. There is a comprehensive bebliography and index. The book addresses prospective users of Isabelle as well as researchers in logic and automated reasoning.
410  0$aLecture Notes in Computer Science,$x0302-9743 ;$v828
606   $aMathematical logic
606   $aComputer logic
606   $aSoftware engineering
606   $aArtificial intelligence
606   $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048
606   $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X
606   $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029
606   $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000
606   $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005
615  0$aMathematical logic.
615  0$aComputer logic.
615  0$aSoftware engineering.
615  0$aArtificial intelligence.
615 14$aMathematical Logic and Formal Languages.
615 24$aLogics and Meanings of Programs.
615 24$aSoftware Engineering.
615 24$aArtificial Intelligence.
615 24$aMathematical Logic and Foundations.
676   $a511.3/0285/53
700   $aPaulson$b Lawrence C$4aut$4http://id.loc.gov/vocabulary/relators/aut$062096
701   $aNipkow$b Tobias$f1958-$062010
906   $aBOOK
912   $a996466091903316
996   $aIsabelle$92860225
997   $aUNISA