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: | Nevins, Arthur J. |
---|---|
Language: | en_US |
Published: |
2004
|
Online Access: | http://hdl.handle.net/1721.1/6217 |
Similar Items
-
Model-Driven Geometry Theorem Prover
by: Ullman, Shimon
Published: (2004) -
An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support
by: Ralph-Johan Back, et al.
Published: (2012-02-01) -
An equality theorem prover based on grammar rewriting
by: Batzoglou, Serafim
Published: (2007) -
Formalization of the Integral Calculus in the PVS Theorem Prover
by: Ricky Wayne Butler
Published: (2009-04-01) -
Reasoning with Inductively Defined Relations in the HOL Theorem Prover
by: Camilleri, J, et al.
Published: (1992)