Discovery of geometry theorems: avoiding isomorphic situation descriptions

Automation of systematic theorem discovery in geometry is still a relatively unexplored area. The authors have recently developed a "generate-and-test" method that combines incremental generation of geometric situation descriptions with a prover to test their consistency; descriptions found to be inconsistent lead to theorems. However, large number of isomorphic descriptions of geometry situations cause the combinatorial complexity of that method to be very high. This paper outlines that method and presents an algorithm that avoids generation of isomorphic descriptions. This is performed by associating permutations with the arguments of each predicate symbol, under which literals involving that predicate symbol preserve their meaning.