文件名称：Applied Logic for Computer Scientist
文件大小：1.88MB
文件格式：PDF
更新时间：2022-05-26 11:57:10
逻辑
计算机方向需要的逻辑理论 This book focuses on two styles of deductive rules: Natural deduction and Gentzen’s calculus. The former is usually considered closer to the mathematical reasoning practice and yields a declarative style of proofs where conclusions follow from assumptions. The latter is closer to the goal-oriented proof construction mechanism used in many interactive theorem provers and yields a more procedural style of proofs. Despite their differences, both styles have the same deductive power. The book introduces classical propositional and predicate logics in both styles along with their completeness and correctness properties. It also briefly discusses constructive variants of these logics and their relations to simply typed lambda calculus. Finally, the last part of the book illustrates how these proof-theoretical concepts are used in the verification of algorithms specified in the Prototype Verification System (PVS)