000 03735nam a22004215i 4500
999 _c361748
_d361748
_x1
001 361748
003 ES-MaUEC
005 20230102121425.0
006 a||||fo|||| 00| 0
007 cr nn nnnaamaa
008 211203s2021 sz | s |||| 0|eng d
020 _a9783030878825
024 7 _a10.1007/978-3-030-87882-5
_2doi
040 _aES-MaUEC
_bspa
_cES-MaUEC
_dES-MaUEC
050 4 _aQA76.9 .L63
_b2021 EB
100 1 _aHou, Zhe
_9682220
245 1 0 _aFundamentals of Logic and Computation :
_bWith Practical Automated Reasoning and Verification
_cby Zhe Hou.
250 _aFirst edition 2021
264 1 _aCham
_bSpringer International Publising
_c2021
300 _a1 recurso en línea (X, 222 páginas)
_b34 ilustraciones, 6 ilustraciones a color
336 _2rdacontent
_aTexto
_btxt
337 _2rdamedia
_aelectrónico
_bc
338 _2rdacarrier
_arecurso electrónico
_bcr
347 _aarchivo de texto
_bPDF
490 0 _aTexts in Computer Science
_x1868-095X
490 0 _aComputer Science (SpringerNature-11645)
490 0 _aComputer Science (R0) (SpringerNature-43710)
505 0 _a1. Introduction to Logic -- 2. First-order Logic -- 3. Non-classical Logics -- 4. Automata Theory and Formal Languages -- 5. Turing Machines and Computability -- 6. Logic is Computation.
520 3 _aAlthough the fields of logic and computation are intrinsically related, most courses treat the two topics separately. This unique textbook aims to compress and unify important concepts of logical reasoning and computational theory, facilitating an in-depth understanding. Delivering theory with practical approaches, the book features early chapters accompanied by exercises in Isabelle/HOL, a popular and user-friendly theorem prover. Latter chapters address modelling and verification in Process Analysis Toolkit (PAT), a feature-rich model checker based on Hoare's Communicating Sequential Processes. The exposition focuses on the syntax, semantics and proof theory of various logics, as well as on automata theory, formal languages, computability, and complexity. It also builds a hybrid skill set of practical theorem proving and model checking, which will provide a solid grounding for future research or work involving formal methods. Topics and features: Offers a transition from logic to computation via linear temporal logic and state machines Includes exercises from widely-used software applications Provides entry-level tutorials for Isabelle/HOL and PAT Employs many examples from the Archives of Formal Proofs, as well as many examples of PAT models Introduces classical and nonclassical logics in an integrated presentation Discusses lambda calculus, recursive functions and Turing machines Concludes by addressing the Curry-Howard correspondence, which unifies logic and computation The work is optimal for undergraduate students striving for a degree in computer science. In addition, it will be an excellent foundational volume for research students considering higher-degree research programs. Zhe Hou is a lecturer in the School of Information and Communication Technology at Griffith University, Nathan, Australia. His research pursuits include explainable AI, autonomous systems, formal verification, and automated reasoning.
988 _aSpringer_Computer_2021
650 7 _2embne
_9139573
_aLógica
776 0 8 _iPrinted edition:
_z9783030878818
776 0 8 _iPrinted edition:
_z9783030878832
776 0 8 _iPrinted edition:
_z9783030878849
856 4 0 _uhttps://go.openathens.net/redirector/universidadeuropea.es?url=https://doi.org/10.1007/978-3-030-87882-5
_zAcceso a este recurso digital (usuarios Universidad Europea de Madrid)
942 _2lcc
_cLE
998 _b02/2022
_dz
_eh
_zSI