{"id":21043,"date":"2023-02-13T02:16:50","date_gmt":"2023-02-13T02:16:50","guid":{"rendered":"https:\/\/www.booksofall.com\/ja\/?post_type=product&#038;p=21043"},"modified":"2023-02-13T02:17:09","modified_gmt":"2023-02-13T02:17:09","slug":"isabelle-hol-a-proof-assistant-for-higher-order-logic","status":"publish","type":"product","link":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/","title":{"rendered":"Isabelle\/HOL &#8211; A Proof Assistant for Higher-Order Logic"},"content":{"rendered":"<p>This volume is a self-contained introduction to interactive proof in <a href=\"https:\/\/en.wikipedia.org\/wiki\/Higher-order_logic\">higherorder logic<\/a> (HOL), using the proof assistant Isabelle. It is written for potential users rather than for our colleagues in the research world. The book has three parts.<\/p>\n<ul>\n<li>The first part, <a href=\"https:\/\/mathworld.wolfram.com\/ElementaryMethods.html\">Elementary Techniques<\/a>, shows how to model functional programs in higher-order logic. Early examples involve lists and natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion.<\/li>\n<li>The second part, Logic and Sets, presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes <a href=\"https:\/\/isabelle.in.tum.de\/\">Isabelle\/HOL<\/a>\u2019s treatment of sets, functions and relations and explains how to define sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.<\/li>\n<li>The third part, Advanced Material, describes a variety of other topics. Among these are the real numbers, records, and overloading. Advanced techniques for induction and recursion are described. A whole chapter is devoted to an extended example: the verification of a security protocol.<\/li>\n<\/ul>\n<p>The typesetting relies on Wenzel\u2019s theory presentation tools. An annotated source file is run, typesetting the theory in the form of a <a href=\"https:\/\/www.latex-project.org\/\">LATEX<\/a> source file. This book is derived almost entirely from the output generated in this way. The final chapter of Part I explains how users may produce their own formal documents in a similar fashion.<\/p>\n<p>Isabelle\u2019s website contains links to the download area and to documentation and other information. The classic Isabelle user interface is <a href=\"https:\/\/proofgeneral.github.io\/\">Proof General<\/a> \/ Emacs by David Aspinall\u2019s. This book says very little about Proof General, which has its own documentation.<\/p>\n<p>This tutorial owes a lot to the constant discussions with and the valuable feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M\u00fcller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch, Norbert Schirmer, and Martin Strecker. Stephan Merz was also kind enough to read and comment on a draft version. We received comments from Stefano Bistarelli, Gergely Buday, John Matthews, and Tanja Vos<\/p>\n","protected":false},"excerpt":{"rendered":"<p><iframe style=\"width: 100%; height: 700px; border: none;\" src=\"https:\/\/online.visual-paradigm.com\/share\/book\/concrete-semantics-1983evu58p?enforceShowPromotionBar=true&amp;p=1\" frameborder=\"0\" allowfullscreen=\"allowfullscreen\"><\/iframe><\/p>\n","protected":false},"featured_media":21047,"template":"","meta":{"_yoast_wpseo_title":"","_yoast_wpseo_metadesc":""},"product_brand":[],"product_cat":[329],"product_tag":[],"class_list":{"0":"post-21043","1":"product","2":"type-product","3":"status-publish","4":"has-post-thumbnail","6":"product_cat-isabelle-hol","8":"first","9":"instock","10":"shipping-taxable","11":"product-type-simple"},"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.1.1 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Isabelle\/HOL - A Proof Assistant for Higher-Order Logic - BooksOfAll Japanese<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/\" \/>\n<meta property=\"og:locale\" content=\"ja_JP\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic - BooksOfAll Japanese\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/\" \/>\n<meta property=\"og:site_name\" content=\"BooksOfAll Japanese\" \/>\n<meta property=\"article:modified_time\" content=\"2023-02-13T02:17:09+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:image\" content=\"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png\" \/>\n<meta name=\"twitter:label1\" content=\"\u63a8\u5b9a\u8aad\u307f\u53d6\u308a\u6642\u9593\" \/>\n\t<meta name=\"twitter:data1\" content=\"2\u5206\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/\",\"url\":\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/\",\"name\":\"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic - BooksOfAll Japanese\",\"isPartOf\":{\"@id\":\"https:\/\/www.booksofall.com\/ja\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png\",\"datePublished\":\"2023-02-13T02:16:50+00:00\",\"dateModified\":\"2023-02-13T02:17:09+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#breadcrumb\"},\"inLanguage\":\"ja\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"ja\",\"@id\":\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#primaryimage\",\"url\":\"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png\",\"contentUrl\":\"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png\",\"width\":\"443\",\"height\":\"642\"},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/www.booksofall.com\/ja\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Categories\",\"item\":\"https:\/\/www.booksofall.com\/ja\/categories\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Isabelle\/HOL &#8211; A Proof Assistant for Higher-Order Logic\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.booksofall.com\/ja\/#website\",\"url\":\"https:\/\/www.booksofall.com\/ja\/\",\"name\":\"BooksOfAll Japanese\",\"description\":\"Biggest IT eBooks library and learning resources - Free eBooks for programming, computing, artificial intelligence and more.\",\"publisher\":{\"@id\":\"https:\/\/www.booksofall.com\/ja\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/www.booksofall.com\/ja\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"ja\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/www.booksofall.com\/ja\/#organization\",\"name\":\"BooksOfAll Japanese\",\"url\":\"https:\/\/www.booksofall.com\/ja\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"ja\",\"@id\":\"https:\/\/www.booksofall.com\/ja\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2022\/06\/booksofall-logo-2.png\",\"contentUrl\":\"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2022\/06\/booksofall-logo-2.png\",\"width\":166,\"height\":30,\"caption\":\"BooksOfAll Japanese\"},\"image\":{\"@id\":\"https:\/\/www.booksofall.com\/ja\/#\/schema\/logo\/image\/\"}}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic - BooksOfAll Japanese","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/","og_locale":"ja_JP","og_type":"article","og_title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic - BooksOfAll Japanese","og_url":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/","og_site_name":"BooksOfAll Japanese","article_modified_time":"2023-02-13T02:17:09+00:00","og_image":[{"url":"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png","type":"","width":"","height":""}],"twitter_card":"summary_large_image","twitter_image":"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png","twitter_misc":{"\u63a8\u5b9a\u8aad\u307f\u53d6\u308a\u6642\u9593":"2\u5206"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/","url":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/","name":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic - BooksOfAll Japanese","isPartOf":{"@id":"https:\/\/www.booksofall.com\/ja\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#primaryimage"},"image":{"@id":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#primaryimage"},"thumbnailUrl":"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png","datePublished":"2023-02-13T02:16:50+00:00","dateModified":"2023-02-13T02:17:09+00:00","breadcrumb":{"@id":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#breadcrumb"},"inLanguage":"ja","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/"]}]},{"@type":"ImageObject","inLanguage":"ja","@id":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#primaryimage","url":"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png","contentUrl":"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2023\/02\/img_63e99d83b45e5.png","width":"443","height":"642"},{"@type":"BreadcrumbList","@id":"https:\/\/www.booksofall.com\/ja\/isabelle-hol-a-proof-assistant-for-higher-order-logic\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.booksofall.com\/ja\/"},{"@type":"ListItem","position":2,"name":"Categories","item":"https:\/\/www.booksofall.com\/ja\/categories\/"},{"@type":"ListItem","position":3,"name":"Isabelle\/HOL &#8211; A Proof Assistant for Higher-Order Logic"}]},{"@type":"WebSite","@id":"https:\/\/www.booksofall.com\/ja\/#website","url":"https:\/\/www.booksofall.com\/ja\/","name":"BooksOfAll Japanese","description":"Biggest IT eBooks library and learning resources - Free eBooks for programming, computing, artificial intelligence and more.","publisher":{"@id":"https:\/\/www.booksofall.com\/ja\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.booksofall.com\/ja\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"ja"},{"@type":"Organization","@id":"https:\/\/www.booksofall.com\/ja\/#organization","name":"BooksOfAll Japanese","url":"https:\/\/www.booksofall.com\/ja\/","logo":{"@type":"ImageObject","inLanguage":"ja","@id":"https:\/\/www.booksofall.com\/ja\/#\/schema\/logo\/image\/","url":"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2022\/06\/booksofall-logo-2.png","contentUrl":"https:\/\/www.booksofall.com\/ja\/wp-content\/uploads\/sites\/4\/2022\/06\/booksofall-logo-2.png","width":166,"height":30,"caption":"BooksOfAll Japanese"},"image":{"@id":"https:\/\/www.booksofall.com\/ja\/#\/schema\/logo\/image\/"}}]}},"_links":{"self":[{"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/product\/21043","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/product"}],"about":[{"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/types\/product"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/media\/21047"}],"wp:attachment":[{"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/media?parent=21043"}],"wp:term":[{"taxonomy":"product_brand","embeddable":true,"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/product_brand?post=21043"},{"taxonomy":"product_cat","embeddable":true,"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/product_cat?post=21043"},{"taxonomy":"product_tag","embeddable":true,"href":"https:\/\/www.booksofall.com\/ja\/wp-json\/wp\/v2\/product_tag?post=21043"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}