Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
From MaRDI portal
Publication:2817933
DOI10.1007/978-3-319-40229-1_23zbMath1475.68450OpenAlexW2460200316MaRDI QIDQ2817933
Martin Möhrmann, Stephan Schulz
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-40229-1_23
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (17)
Vampire with a brain is a good ITP hammer ⋮ Teaching Automated Theorem Proving by Example: PyRes 1.2 ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ 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 ⋮ Layered clause selection for theory reasoning (short paper) ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Lightweight relevance filtering for machine-generated resolution problems
- Limited resource strategy in resolution theorem proving
- Recording and analysing knowledge-based distributed deduction processes
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- System Description: E 1.8
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- System Description: Spass Version 3.0
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Sine Qua Non for Large Theory Reasoning
- A Machine-Oriented Logic Based on the Resolution Principle
This page was built for publication: Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving