source: CGBLisp/examples/prover-pappus.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: 440 bytes
Line 
1;;----------------------------------------------------------------
2;; Encoding of the Pappus theorem in the formalism
3;; implemented in the PROVER package.
4;;----------------------------------------------------------------
5(prove-theorem
6 ((collinear X Y Z)
7 (collinear X P V)
8 (collinear U P Y)
9 (collinear Y R W)
10 (collinear Z R V)
11 (collinear U Q Z)
12 (collinear X Q W)
13 (collinear U V W))
14 ((collinear P Q R))
15 :order #'grevlex>)
Note: See TracBrowser for help on using the repository browser.