Exploiting parallelism: highly competitive semantic tree theorem prover

DOI10.1080/03057920412331272207MaRDI QIDQ4823345zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Recommendations

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

Cites work

• scientific article; zbMATH DE number 1566502 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Hard examples for resolution
• Heuristics used by HERBY for semantic tree theorem proving
• Seventy-five problems for testing automatic theorem provers
• The TPTP problem library. CNF release v1. 2. 1
• The Unit Proof and the Input Proof in Theorem Proving
• The practicality of generating semantic trees for proofs of unsatisfiability

Cited in

(3)

• scientific article; zbMATH DE number 4180829 (Why is no real title available?)
• Parallelization of a hyper-linking-based theorem prover
• PARTHENON: A parallel theorem prover for non-horn clauses

Describes a project that uses

Uses Software

• PrHERBY
• HERBY
• Gandalf
• HOL
• TPTP

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)