Input Transformations and Resolution Implementation Techniques for Theorem Proving in First-Order Logic (Clause Form, Discrimination Networks, Heuristic Search, Locking Resolution)

Greenbaum, Steven

Permalink

https://hdl.handle.net/2142/69558 Copy

Description

Title

Input Transformations and Resolution Implementation Techniques for Theorem Proving in First-Order Logic (Clause Form, Discrimination Networks, Heuristic Search, Locking Resolution)

Author(s)

Greenbaum, Steven

Issue Date

1986

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

Computer Science

Abstract

• This thesis describes a resolution based theorem prover designed for users with little or no knowledge of automated theorem proving. The prover is intended for high speed solution of small to moderate sized problems, usually with no user guidance. This contrasts with many provers designed to use substantial user guidance to solve hard or very hard problems, often having huge search spaces. Such provers are often weak when used without user interaction. Many of our methods should be applicable to large systems as well.
• Our prover uses a restricted form of locking resolution, together with an additional resolution step. Pending resolvents are ordered using a priority-based search strategy which considers a number of factors, including clause complexity measures, derivation depth of the pending resolvent, and other features.
• Also described are transformations that convert formulas from one to another. One is a nonstandard clause-form translation which often avoids the loss of structure and increase in size resulting from the conventional translation, and also takes advantage of repeated subexpressions. Another transformation replaces operators in first-order formulas with their first-order definitions, before translation to clause form. This works particularly well with the nonstandard clause-form translation. There is also a translation from clauses to other clauses that, when coupled with some prover extensions, is useful for theorem proving with equality. The equality method incorporates Knuth-Bendix completion into the proof process to help simplify the search.
• Some implementation methods are described. Data structures that allow fast clause storage and lookup, and efficient implementation of various deletion methods, are discussed. A modification of discrimination networks is described in detail.

Graduation Semester

1986

Type of Resource

text

Permalink

http://hdl.handle.net/2142/69558

Owning Collections