23
Views
0
CrossRef citations to date
0
Altmetric
Miscellany

Exploiting parallelism: highly competitive semantic tree theorem prover

Pages 1051-1067 | Received 18 Feb 2004, Published online: 25 Jan 2007

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 .

Reprints and Corporate Permissions

Please note: Selecting permissions does not provide access to the full text of the article, please see our help page How do I view content?

To request a reprint or corporate permissions for this article, please click on the relevant link below:

Academic Permissions

Please note: Selecting permissions does not provide access to the full text of the article, please see our help page How do I view content?

Obtain permissions instantly via Rightslink by clicking on the button below:

If you are unable to obtain permissions via Rightslink, please complete and submit this Permissions form. For more information, please visit our Permissions help page.