Exploiting parallelism: highly competitive semantic tree theorem prover

DOI10.1080/03057920412331272207zbMATH Open1082.68103OpenAlexW2019170811MaRDI QIDQ4823345FDOQ4823345

Authors: Choon Kyu Kim 

Publication date: 27 October 2004

Published in: International Journal of Computer Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/03057920412331272207

Recommendations

• PARTHENON: A parallel theorem prover for non-horn clauses
• scientific article; zbMATH DE number 4180829
• scientific article
• Heuristics used by HERBY for semantic tree theorem proving
• Parallelization of a hyper-linking-based theorem prover

Mathematics Subject Classification ID

Cites Work

• The TPTP problem library. CNF release v1. 2. 1
• Heuristics used by HERBY for semantic tree theorem proving
• Title not available (Why is that?)
• Hard examples for resolution
• Title not available (Why is that?)
• The Unit Proof and the Input Proof in Theorem Proving
• Seventy-five problems for testing automatic theorem provers
• The practicality of generating semantic trees for proofs of unsatisfiability

Cited In (3)

• Title not available (Why is that?)
• Parallelization of a hyper-linking-based theorem prover
• PARTHENON: A parallel theorem prover for non-horn clauses

Uses Software

• TPTP
• HOL
• Gandalf
• HERBY
• PrHERBY

This page was built for publication: Exploiting parallelism: highly competitive semantic tree theorem prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4823345)