A Relaxation Approach to Splitting in an Automatic Theorem Prover
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 whi...
Main Author: | |
---|---|
Language: | en_US |
Published: |
2004
|
Online Access: | http://hdl.handle.net/1721.1/6217 |