Theorem Proving by Incrementally Extending Theorem Domain
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.