Cited in
(40)- Blocking and other enhancements for bottom-up model generation methods
- Set of support, demodulation, paramodulation: a historical perspective
- SCL(EQ): SCL for first-order logic with equality
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- scientific article; zbMATH DE number 5914361 (Why is no real title available?)
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- Superposition for bounded domains
- Exploring theories with a model-finding assistant
- Lemma Learning in the Model Evolution Calculus
- Computing finite models by reduction to function-free clause logic
- The TPTP typed first-order form with arithmetic
- Paradox
- Darwin
- FINDER
- DCTP
- SATCHMO
- SCOTT
- Mace4
- iProver-Eq
- iProver
- MGTP
- YAGO
- CLIN
- E-KRHyper
- Geo 2007F
- ModGen
- Peers-mcd
- margrave
- GeoNames
- CPSA
- Razor
- On First-Order Model-Based Reasoning
- Theorem proving for classical logic with partial functions by reduction to Kleene logic
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Finite reasons for safety. Parameterized verification by finite model finding
- MACE4 and SEM: a comparison of finite model generators
- Exploiting symmetry in SMT problems
- Model finding for recursive functions in SMT
- Constraint solving for finite model finding in SMT solvers
This page was built for software: E-Darvin
