Skip to main content

Automated Theorem Proving: A Logical Basis

  • 1st Edition - January 1, 1978
  • Author: D.W. Loveland
  • Language: English
  • eBook ISBN:
    9 7 8 - 1 - 4 8 3 2 - 9 6 7 7 - 7

Fundamental Studies in Computer Science, Volume 6: Automated Theorem Proving: A Logical Basis aims to organize, augment, and record the major conceptual advances in automated… Read more

Automated Theorem Proving: A Logical Basis

Purchase options

Limited Offer

Save 50% on book bundles

Immediately download your ebook while waiting for your print delivery. No promo code is needed.

Institutional subscription on ScienceDirect

Request a sales quote
Fundamental Studies in Computer Science, Volume 6: Automated Theorem Proving: A Logical Basis aims to organize, augment, and record the major conceptual advances in automated theorem proving. The publication first examines the role of logical systems and basic resolution. Discussions focus on the Davis-Putnam procedure, ground resolution, semantic trees, general resolution procedure, basic concepts of first-order logic, refutation procedures, and preparation of formulas. The text then takes a look at the refinements of resolution, including unit preference and set-of-support, ordered clause deductions, and setting and linear refinements. The monograph tackles subsumption, resolution with equality, and resolution and problem reduction format. Topics include problem reduction format, paramodulation and linear refinements, paramodulation, and subsumption for linear and nonlinear procedures. The publication is a dependable reference for students and researchers interested in automated theorem proving.