References
References
- Al-Anjawi A (2000) Using demodulation in semantic tree theorem provers ICCI2000 November
- Almulla M (1995) Analysis of the use of semantic trees in automated theorem proving Ph.D. Thesis, School of Computer Science, McGill University Montreal Canada
- Almulla , M and Newborn , M . (1996) . The practicality of generating semantic trees for proofs of unsatisfiability . Int. J. Comp. Math. , 62 : 45 – 61 .
- Almulla M Newborn M (1998) http://www.cs.miami.edu/~tptp/CASC/15
- Chang , CL . (1970) . The unit proof and the input proof in theorem proving . J. ACM , 17 ( 4 ) : 698 – 707 .
- Chang CL Lee RCT (1973) Symbolic Logic and Mechanical Theorem Proving, Academic Press
- Giest A Beguelin A Dongarra J Jiang W Manchek R Sunderam V (1994) PVM: parallel virtual machine A User's Guide and Tutorials for Networked Parallel Computing, MIT Press
- Hurd J (1999) Integrating gandalf and HOL, TPHOLs'99 LNCS 1690 311 321
- Kim CK (2004) Parallel semantic tree theorem proving with resolutions Ph.D. Thesis, School of Computer Science, McGill University Montreal Canada To appear
- Kim CK Newborn M (2003) Competitive semantic tree theorem prover with resolutions, EuroPVM/MPI
- Korf RE (1985) Depth-first iterative-deepening: an Optimal admissible tree search Artificial Intelligence 97 109
- Newborn M (1998) http://www.cs.miami.edu/~tptp/CASC/15/SystemDescriptions.html#TGTP
- Newborn M (2001) Automated Theorem Proving: Theory and Practice, Springer-Verlag
- Pelletier , FJ . (1986) . Seventy-five problems for testing automatic theorem provers . Journal of Automated Reasoning , 2 : 191 – 216 .
- Plaisted DA (1976) Theorem proving and semantic trees Ph.D. Thesis, Stanford University
- Schumann , J . (1997) . SiCoTHEO-simple competitive parallel theorem provers based on SETHEO . Parallel Processing for Artificial Intelligence , 3 : 231 – 245 .
- Sutcliffe , G and Suttner , CB . (1998) . The TPTP problem library . Journal of Automated Reasoning , 21 ( 2 ) : 177 – 203 .
- Yu , Q , Almulla , M and Newborn , M . (1998) . Heuristics used by HERBY for semantic tree theorem proving . Annals of Mathematics and Artificial Intelligence , 23 ( 3 ) : 247 – 266 .
- Urquhart , A . (1987) . Hard examples for resolution . Journal of the ACM , 34 ( 1 ) : 209 – 219 .