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...
| Published in: | Journal of symbolic computation. 25, 2 (1998). |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | English |