Cooperating proof attempts

DOI10.1007/978-3-319-21401-6_23MaRDI QIDQ3454105zbMATH OpenOpenAlexFDO

Authors Giles Reger, Dmitry Tishkovsky, Andrei Voronkov

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-21401-6_23

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• AVATAR: The Architecture for First-Order Theorem Provers
• Playing with AVATAR
• scientific article; zbMATH DE number 1301751
• Cooperation in heterogeneous theorem prover networks (Diss., Univ. Kaiserslautern)
• Parallel cooperative propositional theorem proving

Cites work

• A taxonomy of parallel strategies for deduction
• AVATAR: The Architecture for First-Order Theorem Provers
• E-MaLeS 1.1
• Evaluating general purpose automated theorem proving systems
• Limited resource strategy in resolution theorem proving
• Parallelizing the closure computation in automated deduction
• Partheo: A high-performance parallel theorem prover
• Playing with AVATAR
• Resolution theorem proving
• Sledgehammer: judgement day
• System description: E 1.8
• The 481 ways to split a clause and deal with propositional variables
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(4)

• Playing with AVATAR
• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
• A unifying splitting framework
• Lemmas: generation, selection, application

Describes a project that uses

Uses Software

• DISCOUNT
• E-MaLeS
• E Theorem Prover
• PARTHEO
• Sledgehammer
• TPTP
• VAMPIRE

This page was built for publication: Cooperating proof attempts

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