Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs (Undergraduate Topics in Computer Science)
暫譯: 計算機科學的應用邏輯:計算推理與形式證明(計算機科學本科主題)

Mauricio Ayala-Rincón, Flávio L. C. de Moura

  • 出版商: Springer
  • 出版日期: 2017-02-13
  • 售價: $2,230
  • 貴賓價: 9.5$2,119
  • 語言: 英文
  • 頁數: 150
  • 裝訂: Paperback
  • ISBN: 3319516515
  • ISBN-13: 9783319516516
  • 相關分類: Computer-Science
  • 海外代購書籍(需單獨結帳)

商品描述

This book provides an introduction to logic and mathematical induction which are the basis of any deductive computational framework. A strong mathematical foundation of the logical engines available in modern proof assistants, such as the PVS verification system, is essential for computer scientists, mathematicians and engineers to increment their capabilities to provide formal proofs of theorems and to certify the robustness of software and hardware systems.

The authors present a concise overview of the necessary computational and mathematical aspects of ‘logic’, placing emphasis on both natural deduction and sequent calculus. Differences between constructive and classical logic are highlighted through several examples and exercises. Without neglecting classical aspects of computational logic, the authors also highlight the connections between logical deduction rules and proof commands in proof assistants, presenting simple examples of formalizations of the correctness of algebraic functions and algorithms in PVS.    

Applied Logic for Computer Scientists will not only benefit students of computer science and mathematics but also software, hardware, automation, electrical and mechatronic engineers who are interested in the application of formal methods and the related computational tools to provide mathematical certificates of the quality and accuracy of their products and technologies. 

商品描述(中文翻譯)

本書介紹了邏輯和數學歸納法,這些是任何演繹計算框架的基礎。對於計算機科學家、數學家和工程師來說,現代證明助手中可用的邏輯引擎(如 PVS 驗證系統)所需的強大數學基礎對於增強他們提供定理的正式證明和認證軟體及硬體系統的穩健性至關重要。

作者對“邏輯”的必要計算和數學方面進行了簡明的概述,強調自然推理和序列演算。通過幾個例子和練習,突顯了建構邏輯和古典邏輯之間的差異。在不忽視計算邏輯的古典方面的同時,作者還強調了邏輯推理規則與證明助手中的證明命令之間的聯繫,並展示了在 PVS 中對代數函數和算法正確性的形式化的簡單例子。

《計算機科學家的應用邏輯》不僅將使計算機科學和數學的學生受益,還將使對應用形式方法及相關計算工具感興趣的軟體、硬體、自動化、電氣和機電工程師受益,幫助他們提供產品和技術質量及準確性的數學證明。

最後瀏覽商品 (20)