Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions
Case splitting, with and without backtracking, is compared with straightforward ordered resolution. Both forms of splitting have been implemented for MetiTarski, an automatic theorem prover for real-valued special functions such as , ln , sin, cos and tan (-aEuro parts per thousand 1). The experimental findings confirm the superiority of true backtracking over the simulation of backtracking through the introduction of new predicate symbols, and the superiority of both over straightforward resolution.
splitting metitarski resolution theorem proving spass