The Use of Proof Planning for Co-operative Theorem Proving.
We describeImage : a co-operative interface to theImage inductive theorem proving system. For the foreseeable future, there will be theorems which cannot be proved completely automatically, so the ability to allow human intervention is desirable; for this intervention to be productive the problem of...
| Izdano u: | Journal of symbolic computation. 25, 2 (1998). |
|---|---|
| Glavni autor: | |
| Format: | Članak |
| Jezik: | engleski |