Por qué?
T.R.-P. Velez: Automatic discovery of theorems in elementary geometry, Journal of Automated Reasoning, 1999.
H ==> T
Does not?
Look for R', R'' such that
• H & R' & not R'' ==> T
• expressed in the right variables
• H & T ==> R'
FSDIC
Existence, Unicity
Meaning
Two examples