source: CGBLisp/examples/apollonius0.lisp@ 1

Last change on this file since 1 was 1, checked in by Marek Rychlik, 15 years ago

First import of a version circa 1997.
File size: 348 bytes
Line 
1;; An automatic proof of the Apollonius Circle Theorem
2;; Encoding by hand
3(setf vars '(x1 x2))
4(setf params '(u1 u2))
5(setf allvars (append vars params))
6(setf hypotheses "[x1*u1-x2*u2, -x1*u2-u1*x2+u1*u2]")
7(setf conclusions "[2*x2^2-u2*x2+2*x1^2-u1*x1,u1,u2]")
8;; Saturation test
9(string-ideal-polysaturation-1 hypotheses conclusions allvars)
10
Note: See TracBrowser for help on using the repository browser.