An efficient subsumption test pipeline for BS(LRA) clauses
From MaRDI portal
Publication:2104505
DOI10.1007/978-3-031-10769-6_10OpenAlexW4289103998MaRDI QIDQ2104505
Lorenz Leutgeb, Christoph Weidenbach, Martin Bromberger
Publication date: 7 December 2022
Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_10
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Subsumption and implication
- A theory of timed automata
- Refutational theorem proving for hierarchic first-order theories
- Fast term indexing with coded context trees
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Superposition as a decision procedure for timed automata
- Superposition decides the first-order logic fragment over ground theories
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Subsumption demodulation in first-order theorem proving
- CrystalBall: gazing in the black box of SAT solving
- Hierarchic superposition revisited
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- SPASS-SATT. A CDCL(LA) solver
- SCL clause learning from simple models
- Efficient instance retrieval with standard and relational path indexing
- Fast Cube Tests for LIA Constraint Solving
- Fingerprint Indexing for Paramodulation and Rewriting
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
- Superposition Modulo Non-linear Arithmetic
- Automated Reasoning Building Blocks
- Integrating Linear Arithmetic into Superposition Calculus
- Superposition Modulo Linear Arithmetic SUP(LA)
- On the efficiency of subsumption algorithms
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- A new solution of Dijkstra's concurrent programming problem
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Substitution tree indexing
- The Concept of Weak Substitution in Theorem-Proving
- Extended path-indexing
- A Machine-Oriented Logic Based on the Resolution Principle
- Fast Library for Number Theory: An Introduction
This page was built for publication: An efficient subsumption test pipeline for BS(LRA) clauses
