Playing with AVATAR

DOI10.1007/978-3-319-21401-6_28MaRDI QIDQ3454110zbMATH OpenOpenAlexFDO

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

Recommendations

• AVATAR: The Architecture for First-Order Theorem Provers
• Cooperating proof attempts
• The 481 ways to split a clause and deal with propositional variables
• Combining superposition, sorts and splitting
• Labelled splitting

Cites work

• Evaluating general purpose automated theorem proving systems
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• Limited resource strategy in resolution theorem proving
• 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

(21)

• Solving quantified linear arithmetic by counterexample-guided instantiation
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• A unifying splitting framework
• Improving ENIGMA-style clause selection while learning from history
• Larry Wos: visions of automated reasoning
• Set of support, demodulation, paramodulation: a historical perspective
• Faster, higher, stronger: E 2.3
• Super-blocked clauses
• Selecting the selection
• Splitting through new proposition symbols
• Cooperating proof attempts
• Local redundancy in SAT: generalizations of blocked clauses
• The 481 ways to split a clause and deal with propositional variables
• Making higher-order superposition work
• Making higher-order superposition work
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Unifying splitting
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Learning guided automated reasoning: a brief survey
• Lemma discovery and strategies for automated induction
• Vampire with a brain is a good ITP hammer

Describes a project that uses

Uses Software

• VAMPIRE
• MiniSat
• TPTP

This page was built for publication: Playing with AVATAR

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