Layered clause selection for theory reasoning (short paper)
From MaRDI portal
Publication:2096461
DOI10.1007/978-3-030-51074-9_23OpenAlexW3038732795MaRDI QIDQ2096461
Publication date: 9 November 2022
Full work available at URL: https://arxiv.org/abs/2001.09705
Related Items (9)
Vampire with a brain is a good ITP hammer ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Making theory reasoning simpler ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- Unnamed Item
- Limited resource strategy in resolution theorem proving
- Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Old or heavy? Decaying gracefully with age/weight shapes
- Faster, higher, stronger: E 2.3
- GKC: a reasoning system for large knowledge bases
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
- AVATAR: The Architecture for First-Order Theorem Provers
- Ordered chaining calculi for first-order theories of transitive relations
- Extensional Crisis and Proving Identity
- Superposition Modulo Linear Arithmetic SUP(LA)
- A New Class of Automated Theorem-Proving Algorithms
- Hierarchic Superposition with Weak Abstraction
- Coming to terms with quantified reasoning
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
This page was built for publication: Layered clause selection for theory reasoning (short paper)
