An efficient subsumption test pipeline for BS(LRA) clauses
type: Item
instance of: scholarly article
title: An efficient subsumption test pipeline for BS(LRA) clauses
DOI: 10.1007/978-3-031-10769-6_10
author: Martin Bromberger
author: Lorenz Leutgeb
author: Christoph Weidenbach
publication date: 2022-12-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7628186
zbMATH Keywords: Bernays-Schönfinkel fragment
zbMATH Keywords: linear arithmetic
zbMATH Keywords: redundancy elimination
zbMATH Keywords: subsumption
describes a project that uses: SPASS
describes a project that uses: Chaff
describes a project that uses: OTTER
describes a project that uses: FLINT
describes a project that uses: z3
describes a project that uses: CrystalBall
describes a project that uses: VAMPIRE
MaRDI profile type: Publication
full work available at URL: 978-3-031-10769-6 10
OpenAlex ID: W4289103998
cites work: NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
cites work: Superposition Modulo Linear Arithmetic SUP(LA)
cites work: A theory of timed automata
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Resolution theorem proving
cites work: Refutational theorem proving for hierarchic first-order theories
cites work: Hierarchic superposition revisited
cites work: Q5503674
cites work: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
cites work: Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
cites work: SPASS-SATT. A CDCL(LA) solver
cites work: Fast Cube Tests for LIA Constraint Solving
cites work: Orderings for term-rewriting systems
cites work: Superposition Modulo Non-linear Arithmetic
cites work: Superposition as a decision procedure for timed automata
cites work: SCL clause learning from simple models
cites work: Q5457277
cites work: Fast term indexing with coded context trees
cites work: Subsumption demodulation in first-order theorem proving
cites work: Subsumption and implication
cites work: On the efficiency of subsumption algorithms
cites work: Extended path-indexing
cites work: Substitution tree indexing
cites work: Q4524770
cites work: Fast Library for Number Theory: An Introduction
cites work: Q3696523
cites work: Integrating Linear Arithmetic into Superposition Calculus
cites work: Superposition decides the first-order logic fragment over ground theories
cites work: A new solution of Dijkstra's concurrent programming problem
cites work: Experiments with discrimination-tree indexing and path indexing for term retrieval
cites work: Q4539610
cites work: Paramodulation-based theorem proving
cites work: Q3880317
cites work: Term indexing
cites work: Q4536327
cites work: Efficient instance retrieval with standard and relational path indexing
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q4221106
cites work: Simple and Efficient Clause Subsumption with Feature Vector Indexing
cites work: Fingerprint Indexing for Paramodulation and Rewriting
cites work: Q3804226
cites work: CrystalBall: gazing in the black box of SAT solving
cites work: The Concept of Weak Substitution in Theorem-Proving
cites work: Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
cites work: The anatomy of vampire. Implementing bottom-up procedures with code trees
cites work: Q4539595
cites work: Automated Reasoning Building Blocks
cites work: Otter 2.0
description: scientific article; zbMATH DE number 7628186