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

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2014

Author dc:creator

• Greenbaum, Steven

• Computer Science

Identifier

(UMI)AAI8701496

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/69558