Proof: Difference between revisions
→An unusual use of ATS
Line 222:
=== An unusual use of ATS ===
The following seems similar, at least, to a completion of the task. The main problem I can see in it is it mostly consists of letting ATS do math it already knows on the ''recursion indices'' of the definition of addition. These happen to correspond to the natural numbers abstractly represented by the "prop" '''NATURAL'''.
Nevertheless, one can see that ATS is capable of some "abstract" reasoning. In fact, the prelude includes a recursive definition of multiplication, and in the [[Greatest_common_divisor#ATS|ATS entry for the greatest common divisor task]] I present definitions of the gcd both by way of axioms and by recursive prop.
| |||