Layered clause selection for theory reasoning (short paper)
type: Item
instance of: scholarly article
title: Layered clause selection for theory reasoning (short paper)
DOI: 10.1007/978-3-030-51074-9_23
author: Bernhard Gleiss
author: Martin Suda
publication date: 2022-11-09T00:00:00Z
full work available at URL: https://arxiv.org/abs/2001.09705
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7614525
describes a project that uses: StarExec
describes a project that uses: AVATAR
describes a project that uses: VAMPIRE
describes a project that uses: SMT-LIB
describes a project that uses: SPASS+T
describes a project that uses: OTTER
describes a project that uses: Easychair
MaRDI profile type: Publication
OpenAlex ID: W3038732795
cites work: Superposition Modulo Linear Arithmetic SUP(LA)
cites work: Ordered chaining calculi for first-order theories of transitive relations
cites work: Resolution theorem proving
cites work: Hierarchic Superposition with Weak Abstraction
cites work: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
cites work: Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
cites work: Extensional Crisis and Proving Identity
cites work: Coming to terms with quantified reasoning
cites work: A New Class of Automated Theorem-Proving Algorithms
cites work: Old or heavy? Decaying gracefully with age/weight shapes
cites work: Unification with abstraction and theory instantiation in saturation-based reasoning
cites work: Limited resource strategy in resolution theorem proving
cites work: Faster, higher, stronger: E 2.3
cites work: Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
cites work: GKC: a reasoning system for large knowledge bases
cites work: AVATAR: The Architecture for First-Order Theorem Provers
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
Recommended article: Clause trees: A tool for understanding and implementing resolution in automated reasoning
Recommended article: Q4797349
Recommended article: Q4415137
Recommended article: Layerings of logic programs -- layer decomposable semantics and incremental model computation
Recommended article: Q3753517
Recommended article: Extracting models from clause sets saturated under semantic refinements of the resolution rule.
Recommended article: Q4847004
Recommended article: A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
Recommended article: Layer Supported Models of Logic Programs
Recommended article: Q5414681
description: scientific article; zbMATH DE number 7614525