19. Juni 2013
Human mathematicians prove a theorem by combining individual computation steps. This is a rather trivial task for a computer program once the necessary steps are known. For automatized processes, however, choosing which steps to execute is similar to looking for a needle in an infinitely large haystack. The research group „Automation of Logic“ is one of the world leaders in developing efficient automated theorem provers.