Provided by: International Journal of Emerging Trends & Technology in Computer Science (IJETTCS)
Date Added: Feb 2015
Automated Theorem provers are used to check if the mathematical theorems are proved true or false. If the theorem is true, the automated theorem prover, usually, prints out the proof. In this paper, the authors present a new approach to deal with the other case, i.e. if the theorem is false. The semantic tableau method is used to extend the theorem domain. The modified automated theorem prover suggests an extension of the domain, if it is available, to present a new provable theorem.