Overview
- Provides readers with the fundamental tools needed to develop mathematical certificates of correctness and robustness of software and hardware systems
- Explains how logical deductive rules are related with proof commands available in deductive frameworks such as PVS
- Clarifies the differences between constructive and classical deduction
- Includes supplementary material: sn.pub/extras
Part of the book series: Undergraduate Topics in Computer Science (UTICS)
Access this book
Tax calculation will be finalised at checkout
Other ways to access
Table of contents (6 chapters)
Keywords
About this book
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.
Authors and Affiliations
About the authors
Flávio L. C. de Moura is an Adjunct Professor in Computer Science at the Universidade de Brasília where he received his Ph.D in Mathematics (Theory of Computing). He has done long term research programs at Heriot-Watt University and Université Paris Diderot. His research is focused on lambda calculus and explicit substitutions, and in the application of proof assistants for the formalization of computation and mathematics.
Bibliographic Information
Book Title: Applied Logic for Computer Scientists
Book Subtitle: Computational Deduction and Formal Proofs
Authors: Mauricio Ayala-Rincón, Flávio L. C. de Moura
Series Title: Undergraduate Topics in Computer Science
DOI: https://doi.org/10.1007/978-3-319-51653-0
Publisher: Springer Cham
eBook Packages: Computer Science, Computer Science (R0)
Copyright Information: The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG 2017
Softcover ISBN: 978-3-319-51651-6Published: 13 February 2017
eBook ISBN: 978-3-319-51653-0Published: 04 February 2017
Series ISSN: 1863-7310
Series E-ISSN: 2197-1781
Edition Number: 1
Number of Pages: XVIII, 150
Number of Illustrations: 4 b/w illustrations
Topics: Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Math Applications in Computer Science