Superposition for bounded domains
From MaRDI portal
Recommendations
Cites work
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Combination of disjoint theories: beyond decidability
- Combining superposition, sorts and splitting
- Computing finite models by reduction to function-free clause logic
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- scientific article; zbMATH DE number 1848313 (Why is no real title available?)
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- Labelled splitting
- More SPASS with Isabelle
- New results on rewrite-based satisfiability procedures
- On deciding satisfiability by theorem proving with speculative inferences
- On the saturation of YAGO
- Paramodulation-based theorem proving
- Proof Systems for Effectively Propositional Logic
- Refutational theorem proving for hierarchic first-order theories
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Superposition as a decision procedure for timed automata
- Superposition modulo linear arithmetic SUP(LA)
- The hyper tableaux calculus with equality and an application to finite model computation
- The Isabelle Framework
- Theoretical Aspects of Computing – ICTAC 2005
Cited in
(11)- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Superposition with first-class booleans and inprocessing clausification
- SCL clause learning from simple models
- Superposition for fixed domains
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- scientific article; zbMATH DE number 5857449 (Why is no real title available?)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Superposition for Fixed Domains
- First-order automatic literal model generation
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
Describes a project that uses
Uses Software
This page was built for publication: Superposition for bounded domains
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4913861)
