Improving ENIGMA-style clause selection while learning from history
type: Item
instance of: scholarly article
title: Improving ENIGMA-style clause selection while learning from history
DOI: 10.1007/978-3-030-79876-5_31
author: Martin Suda
publication date: 2021-12-01T00:00:00Z
full work available at URL: https://arxiv.org/abs/2102.13564
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437099
zbMATH Keywords: saturation-based theorem proving
zbMATH Keywords: clause selection
zbMATH Keywords: machine learning
zbMATH Keywords: recursive neural networks
describes a project that uses: MobileNetV2
describes a project that uses: SPASS
describes a project that uses: ENIGMA
describes a project that uses: DeepMath
describes a project that uses: SMT-LIB
MaRDI profile type: Publication
OpenAlex ID: W3186348969
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Resolution theorem proving
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
cites work: Learning domain knowledge to improve theorem proving
cites work: Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
cites work: Layered clause selection for theory reasoning (short paper)
cites work: Q5270493
cites work: ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
cites work: ENIGMA: efficient learning-based inference guiding machine
cites work: Enhancing ENIGMA given clause guidance
cites work: Hammering Mizar by Learning Clause Guidance (Short Paper).
cites work: Coming to terms with quantified reasoning
cites work: Deep Network Guided Proof Search
cites work: Paramodulation-based theorem proving
cites work: Q4999300
cites work: Playing with AVATAR
cites work: Limited resource strategy in resolution theorem proving
cites work: Q5290112
cites work: Learning search control-knowledge for equational deduction
cites work: Faster, higher, stronger: E 2.3
cites work: Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
cites work: Q2934059
cites work: GKC: a reasoning system for large knowledge bases
cites work: AVATAR: The Architecture for First-Order Theorem Provers
description: scientific article; zbMATH DE number 7437099