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