Playing with AVATAR
From MaRDI portal
Recommendations
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
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)