This is an area of research: http://en.wikipedia.org/wiki/Automated_theorem_proving