Coverart for item
The Resource First-Order Logic and Automated Theorem Proving, by Melvin Fitting

First-Order Logic and Automated Theorem Proving, by Melvin Fitting

Label
First-Order Logic and Automated Theorem Proving
Title
First-Order Logic and Automated Theorem Proving
Statement of responsibility
by Melvin Fitting
Creator
Subject
Language
eng
Summary
This graduate-level text presents fundamental concepts and results of classical logic in a rigorous mathematical style. Applications to automated theorem proving are considered and usable Prolog programs provided. It will serve both as a first text in formal logic and an introduction to automation issues for students in computer science or mathematics. The book treats propositional logic, first-order logic, and first-order logic with equality. In each case the initial presentation is semantic, to define the intended subjects independently of the choice of proof mechanism. Then many kinds of proof procedure are introduced. Results such as completeness, compactness, and interpolation are established, and theorem provers are implemented in Prolog. This new edition includes material on AE calculus, Herbrand's Theorem, Gentzen's Theorem, and related topics
Member of
http://library.link/vocab/creatorName
Fitting, Melvin
Dewey number
005.131
Illustrations
illustrations
Index
no index present
Literary form
non fiction
Nature of contents
dictionaries
Series statement
Graduate Texts in Computer Science,
http://library.link/vocab/subjectName
  • Computer science
  • Logic design
  • Logic, Symbolic and mathematical
Label
First-Order Logic and Automated Theorem Proving, by Melvin Fitting
Instantiates
Publication
Antecedent source
file reproduced from original
Bibliography note
Includes bibliographical references (p. [315]-318) and index
Color
mixed
Control code
ocn853258927
Dimensions
unknown
Edition
Second edition
Extent
1 online resource (xvii, 348 pages 15 illustrations)
File format
unknown
Form of item
online
Isbn
9781461223603
Level of compression
uncompressed
Note
SpringerLink
Quality assurance targets
unknown
Reformatting quality
access
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)853258927
Label
First-Order Logic and Automated Theorem Proving, by Melvin Fitting
Publication
Antecedent source
file reproduced from original
Bibliography note
Includes bibliographical references (p. [315]-318) and index
Color
mixed
Control code
ocn853258927
Dimensions
unknown
Edition
Second edition
Extent
1 online resource (xvii, 348 pages 15 illustrations)
File format
unknown
Form of item
online
Isbn
9781461223603
Level of compression
uncompressed
Note
SpringerLink
Quality assurance targets
unknown
Reformatting quality
access
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)853258927

Library Locations

    • InternetBorrow it
      Albany, Auckland, 0632, NZ
Processing Feedback ...