rdf-syntax-grammar
mods:
  schema location: http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
  title info:
    title: First-Order Logic and Automated Theorem Proving
  name:
    name part: Fitting, Melvin.
    role:
      role term: creator
  name:
    name part: SpringerLink (Online service)
  type of resource: text
  genre: Electronic books.
  origin info:
    place:
      place term: nyu
    date issued: 1990
    issuance: monographic
  language:
    language term: eng
  physical description:
    reformatting quality: access
    form: remote
    extent: 1 online resource (xv, 242 pages 26 illustrations)
  abstract: This monograph on classical logic presents fundamental concepts and results in a rigorous mathematical style. Applications to automated theorem proving are considered and usable programs in Prolog are provided. This material can be used 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.
  note: by Melvin Fitting.
  note: Electronic resource.
  subject:
    topic: Computer science
  subject:
    topic: Logic design
  subject:
    topic: Artificial intelligence
  subject:
    topic: Artificial intelligence
  subject:
    topic: Computer science
  subject:
    topic: Logic design
  classification: QA8.9-QA10.3
  classification: 005.131
  related item:
    title info:
      title: Texts and monographs in computer science
  identifier: 9781468403572 (electronic bk.)
  identifier: 1468403575 (electronic bk.)
  identifier: 9781468403596
  identifier: 1468403591
  identifier: http://proxy.library.tamu.edu/login
  record info:
    record content source: AU@
    record creation date: 121227
    record change date: 20260422220045.4
    record identifier: in00003575181
    language of cataloging:
      language term: eng