Metalevel and reflexive extension in mechanical theorem proving
In spite of many years of research into mechanical assistance for mathematics it is still much more difficult to construct a proof on a machine than on paper. Of course this is partly because, unlike a proof on paper, a machine checked proof must be formal in the strictest sense of that word, but it...
| Main Author: | |
|---|---|
| Published: |
University of Edinburgh
1994
|
| Subjects: | |
| Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.657448 |