Octopus: combining learning and parallel search

DOI10.1007/s10817-004-3243-2zbMath1102.68647OpenAlexW1998720940MaRDI QIDQ861370

Zongyan Wang, Monty Newborn

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

Related Items (1)

The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Learning by understanding analogies
• Theorem proving with abstraction
• PARTHENON: A parallel theorem prover for non-horn clauses
• SETHEO: A high-performance theorem prover
• The TPTP problem library. CNF release v1. 2. 1
• SPS-parallelism+SETHEO=SPTHEO
• A taxonomy of parallel strategies for deduction
• Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover
• A paradigm for reasoning by analogy

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