Octopus: combining learning and parallel search

DOI10.1007/S10817-004-3243-2MaRDI QIDQ861370zbMATH OpenOpenAlexFDO

Authors Monty Newborn, Zongyan Wang

Publication date 29 January 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-004-3243-2

zbMATH Keywords

automated theorem provingparallel searchlearning strategies

Mathematics Subject Classification ID

Recommendations

• Automatic Learning of Proof Methods in Proof Planning
• scientific article; zbMATH DE number 1737186
• Improving the time efficiency of proving theorems using a learning mechanism
• scientific article; zbMATH DE number 4164187
• scientific article; zbMATH DE number 1882060

Cites work

• scientific article; zbMATH DE number 1566502 (Why is no real title available?)
• scientific article; zbMATH DE number 4164187 (Why is no real title available?)
• scientific article; zbMATH DE number 4090850 (Why is no real title available?)
• scientific article; zbMATH DE number 1765690 (Why is no real title available?)
• scientific article; zbMATH DE number 924427 (Why is no real title available?)
• A paradigm for reasoning by analogy
• A taxonomy of parallel strategies for deduction
• Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover
• Learning by understanding analogies
• PARTHENON: A parallel theorem prover for non-horn clauses
• SETHEO: A high-performance theorem prover
• SPS-parallelism+SETHEO=SPTHEO
• The TPTP problem library. CNF release v1. 2. 1
• Theorem proving with abstraction

Cited in

(3)

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Improving the time efficiency of proving theorems using a learning mechanism
• scientific article; zbMATH DE number 2090296 (Why is no real title available?)

Describes a project that uses

Uses Software

• Aquarius
• METEOR
• PARTHENON
• Peers-mcd
• SPTHEO
• HERBY
• Bliksem
• DISCOUNT
• EQP
• Roo
• Octopus
• SicoTHEO
• TPTP
• SPASS
• OTTER
• TGTP
• PLAGIATOR
• SETHEO

This page was built for publication: Octopus: combining learning and parallel search

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