kevinsullivan / cs6501s23

Formal Mathematics for Software Design
6 stars 6 forks source link

Example of Automated Reasoning #2

Open nehakrishnakumar opened 1 year ago

nehakrishnakumar commented 1 year ago

"This means, among other things, that one can add points to points in tf without receiving any type errors from the programming language system, even though addition of points to points makes no physical sense and is inconsistent with the abstract mathematics of the domain. In an affine space, there is no operation for adding points to point."

This is more of a request for clarification. Does automating this rule of preventing the addition of a point to a point count as automated reasoning?