Experiments in using a theorem prover to prove and develop geometrical theorems in computer vision

A geometrical theorem prover based on algebraic techniques has been used to prove and derive theorems in computer vision. The results show that theorems relevant to persepective viewing and the properties of shadows can be proven, including some which contain inequalities. Deriving theorems by stating incomplete hypotheses and letting the prover suggest the missing constraints can provide valuable new insights into vision probiems. However, there is no guarantee that the suggestions made by the proof algorithm are interpretable in terms of primitive geometric concepts.