Selecting the Selection

DOI10.1007/978-3-319-40229-1_22zbMath1475.68436arXiv1604.08055OpenAlexW2399785175MaRDI QIDQ2817931

Kryštof Hoder, Martin Suda, Giles Reger, Andrei Voronkov

Publication date: 5 September 2016

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

Full work available at URL: https://arxiv.org/abs/1604.08055

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (10)

Make E Smart Again (Short Paper) ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ Making theory reasoning simpler ⋮ Machine learning guidance for connection tableaux ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Old or heavy? Decaying gracefully with age/weight shapes ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description)

Uses Software

• VAMPIRE
• TPTP
• StarExec
• E Theorem Prover
• AVATAR

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• AVATAR: The Architecture for First-Order Theorem Provers
• Playing with AVATAR
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Selecting the Selection