Books.org participates in affiliate programs including Bookshop.org and the Amazon Services LLC Associates Program. We may earn a commission from qualifying purchases made through links on this page, at no additional cost to you.
Synopsis
This text and software package introduces the reader to automated theorem proving and provides two approaches implemented as easy-to-use programs. The two approaches studied are semantic tree theorem proving and resolution-refutation theorem proving. The first chapters introduce the reader to first-order predicate calculus, well-formed formulae, and their transformation to clauses (implemented in a third program provided on diskette). Then the author shows how the two methods work and provides numerous examples for readers to try their hand at theorem-proving experiments. Each chapter comes with exercises intended to familiarise the readers with the ideas and with the software, and answers are provided to many of the problems.