An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] /

In case you are considering to adopt this book for courses with over 50 students, please contact ties.nijssen@springer.com  for more information. This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.

Saved in:
Bibliographic Details
Main Authors: Andrews, Peter B. author., SpringerLink (Online service)
Format: Texto biblioteca
Language:eng
Published: Dordrecht : Springer Netherlands : Imprint: Springer, 2002
Subjects:Mathematics., Logic., Computers., Artificial intelligence., Mathematical logic., Computational linguistics., Mathematical Logic and Foundations., Computing Methodologies., Artificial Intelligence (incl. Robotics)., Computational Linguistics.,
Online Access:http://dx.doi.org/10.1007/978-94-015-9934-4
Tags: Add Tag
No Tags, Be the first to tag this record!
id KOHA-OAI-TEST:191776
record_format koha
institution COLPOS
collection Koha
country México
countrycode MX
component Bibliográfico
access En linea
En linea
databasecode cat-colpos
tag biblioteca
region America del Norte
libraryname Departamento de documentación y biblioteca de COLPOS
language eng
topic Mathematics.
Logic.
Computers.
Artificial intelligence.
Mathematical logic.
Computational linguistics.
Mathematics.
Mathematical Logic and Foundations.
Computing Methodologies.
Logic.
Artificial Intelligence (incl. Robotics).
Computational Linguistics.
Mathematics.
Logic.
Computers.
Artificial intelligence.
Mathematical logic.
Computational linguistics.
Mathematics.
Mathematical Logic and Foundations.
Computing Methodologies.
Logic.
Artificial Intelligence (incl. Robotics).
Computational Linguistics.
spellingShingle Mathematics.
Logic.
Computers.
Artificial intelligence.
Mathematical logic.
Computational linguistics.
Mathematics.
Mathematical Logic and Foundations.
Computing Methodologies.
Logic.
Artificial Intelligence (incl. Robotics).
Computational Linguistics.
Mathematics.
Logic.
Computers.
Artificial intelligence.
Mathematical logic.
Computational linguistics.
Mathematics.
Mathematical Logic and Foundations.
Computing Methodologies.
Logic.
Artificial Intelligence (incl. Robotics).
Computational Linguistics.
Andrews, Peter B. author.
SpringerLink (Online service)
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] /
description In case you are considering to adopt this book for courses with over 50 students, please contact ties.nijssen@springer.com  for more information. This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.
format Texto
topic_facet Mathematics.
Logic.
Computers.
Artificial intelligence.
Mathematical logic.
Computational linguistics.
Mathematics.
Mathematical Logic and Foundations.
Computing Methodologies.
Logic.
Artificial Intelligence (incl. Robotics).
Computational Linguistics.
author Andrews, Peter B. author.
SpringerLink (Online service)
author_facet Andrews, Peter B. author.
SpringerLink (Online service)
author_sort Andrews, Peter B. author.
title An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] /
title_short An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] /
title_full An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] /
title_fullStr An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] /
title_full_unstemmed An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] /
title_sort introduction to mathematical logic and type theory: to truth through proof [electronic resource] /
publisher Dordrecht : Springer Netherlands : Imprint: Springer,
publishDate 2002
url http://dx.doi.org/10.1007/978-94-015-9934-4
work_keys_str_mv AT andrewspeterbauthor anintroductiontomathematicallogicandtypetheorytotruththroughproofelectronicresource
AT springerlinkonlineservice anintroductiontomathematicallogicandtypetheorytotruththroughproofelectronicresource
AT andrewspeterbauthor introductiontomathematicallogicandtypetheorytotruththroughproofelectronicresource
AT springerlinkonlineservice introductiontomathematicallogicandtypetheorytotruththroughproofelectronicresource
_version_ 1756266240444203008
spelling KOHA-OAI-TEST:1917762018-07-30T23:16:23ZAn Introduction to Mathematical Logic and Type Theory: To Truth Through Proof [electronic resource] / Andrews, Peter B. author. SpringerLink (Online service) textDordrecht : Springer Netherlands : Imprint: Springer,2002.engIn case you are considering to adopt this book for courses with over 50 students, please contact ties.nijssen@springer.com  for more information. This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.0 Introduction -- 1 Propositional Calculus -- 2 First-Order Logic -- 3 Provability and Refutability -- 4 Further Topics in First-Order Logic -- 5 Type Theory -- 6 Formalized Number Theory -- 7 Incompleteness and Undecidability -- Supplementary Exercises -- Summary of Theorems -- List of Figures.In case you are considering to adopt this book for courses with over 50 students, please contact ties.nijssen@springer.com  for more information. This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.Mathematics.Logic.Computers.Artificial intelligence.Mathematical logic.Computational linguistics.Mathematics.Mathematical Logic and Foundations.Computing Methodologies.Logic.Artificial Intelligence (incl. Robotics).Computational Linguistics.Springer eBookshttp://dx.doi.org/10.1007/978-94-015-9934-4URN:ISBN:9789401599344