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...
| Τόπος έκδοσης: | Journal of symbolic computation. 25, 2 (1998). |
|---|---|
| Κύριος συγγραφέας: | |
| Μορφή: | Άρθρο |
| Γλώσσα: | English |