An efficient subsumption test pipeline for BS(LRA) clauses
From MaRDI portal
Publication:2104505
Cites work
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- A Machine-Oriented Logic Based on the Resolution Principle
- A new solution of Dijkstra's concurrent programming problem
- A theory of timed automata
- Automated reasoning building blocks
- CrystalBall: gazing in the black box of SAT solving
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Efficient instance retrieval with standard and relational path indexing
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Extended path-indexing
- Fast cube tests for LIA constraint solving
- Fast Library for Number Theory: An Introduction
- Fast term indexing with coded context trees
- Fingerprint indexing for paramodulation and rewriting
- Hierarchic superposition revisited
- scientific article; zbMATH DE number 3921984 (Why is no real title available?)
- scientific article; zbMATH DE number 4072424 (Why is no real title available?)
- scientific article; zbMATH DE number 3684930 (Why is no real title available?)
- scientific article; zbMATH DE number 1234104 (Why is no real title available?)
- scientific article; zbMATH DE number 1552512 (Why is no real title available?)
- scientific article; zbMATH DE number 1759379 (Why is no real title available?)
- scientific article; zbMATH DE number 1765659 (Why is no real title available?)
- scientific article; zbMATH DE number 1765674 (Why is no real title available?)
- scientific article; zbMATH DE number 5263038 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Integrating Linear Arithmetic into Superposition Calculus
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- On the efficiency of subsumption algorithms
- Orderings for term-rewriting systems
- Otter 2.0
- Paramodulation-based theorem proving
- Refutational theorem proving for hierarchic first-order theories
- Resolution theorem proving
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- SCL clause learning from simple models
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- SPASS-SATT. A CDCL(LA) solver
- Substitution tree indexing
- Subsumption and implication
- Subsumption demodulation in first-order theorem proving
- Superposition as a decision procedure for timed automata
- Superposition decides the first-order logic fragment over ground theories
- Superposition modulo linear arithmetic SUP(LA)
- Superposition modulo non-linear arithmetic
- Term indexing
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- The Concept of Weak Substitution in Theorem-Proving
Cited in
(2)
This page was built for publication: An efficient subsumption test pipeline for BS(LRA) clauses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104505)
