Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving

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

Mathematics Subject Classification ID

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

• OTTER
• VAMPIRE
• SPASS
• TPTP
• Prover9
• Mace4
• StarExec
• E Theorem Prover
• Easychair
• Waldmeister
• DISCOUNT

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