Playing with AVATAR

DOI10.1007/978-3-319-21401-6_28zbMath1465.68295OpenAlexW1472528886MaRDI QIDQ3454110

Martin Suda, Giles Reger, 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_28

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (17)

Vampire with a brain is a good ITP hammer ⋮ Cooperating Proof Attempts ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Unifying splitting ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Unnamed Item ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Super-Blocked Clauses ⋮ Selecting the Selection ⋮ A unifying splitting framework ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Faster, higher, stronger: E 2.3 ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• MiniSat
• VAMPIRE
• TPTP

Cites Work

• Unnamed Item
• Limited resource strategy in resolution theorem proving
• Evaluating general purpose automated theorem proving systems
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The 481 Ways to Split a Clause and Deal with Propositional Variables

This page was built for publication: Playing with AVATAR