A Relaxation Approach to Splitting in an Automatic Theorem Prover,
Abstract
The splitting of a problem into subproblems often involves the same variable appearing in more than one of the subproblems. This makes these subproblems dependent upon one another since a solution to one may not qualify as a solution to another. A two stage method of splitting is described which first obtains solutions by relaxing the dependency requirement and then attempts to reconcile solutions to different subproblems. The method has been realized as part of an automatic theorem prover programmed in LISP.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1974
- Accession Number
- ADA004269
Entities
People
- Arthur J. Nevins
Organizations
- Massachusetts Institute of Technology