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...

Full description

Bibliographic Details
Main Author: Nevins, Arthur J.
Language:en_US
Published: 2004
Online Access:http://hdl.handle.net/1721.1/6217