Obálkyknih.cz - Jihočeská vědecká knihovna v Českých Budějovicích

oprava existující anotace, přidání nové anotace

Název:		First Order Logic Automated Theo (Ima Volumes in Mathematics and Its Applications)
Autor:
Rok vydání:		1990
Identifikátory:		9780387972336

Upravte stávající anotaci nebo vložte anotaci novou.
Anotace:	"First-Order Logic and Automated Theorem Proving" is a treatment of classical logic that presents fundamental concepts and results in a rigorous mathematical style. It also considers applications to automated theorem proving, to the point of providing usable programs (in Prolog). This material will serve both as a first text in formal logic and as an introduction to automation issues, and is intended for those interested in computer science and mathematics at the beginning graduate level. The book begins with propositional logic, then treats first-order logic, and finally, first-order logic with equality. In each case the initial presentation is semantic: Boolean valuations for propositional logic, models for first-order logic, and normal models when equality is added. This defines the intended subjects independently of a particular choice of proof mechanism. Then many kinds of proof procedures are introduced: tableau, resolution, natural deduction, Gentzen sequent and axiom systems. Completeness issues are centered in a Model Existence Theorem, which permits the coverage of a variety of proof procedures without repetition of detail. In addition, results such as Compactness, Interpolation, and the Beth Definability theorem are easily established. Implementations of tableau theorem provers are given in Prolog, and resolution is left as a project for the student. In this new edition, the author has added material on AE calculus, Herbrand's Theorem, Gentzen's Theorem, and related topics.
	Souhlasím s využitím anotace pro potřeby projektu obálkyknih.cz. Obsah neporušuje autorská práva.(povinné)