swMATH6852MaRDI QIDQ18923FDOQ18923
Author name not available (Why is that?)
Official website: http://userpages.uni-koblenz.de/~bpelzer/edarwin/
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
- Title not available (Why is that?)
- 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
- On First-Order Model-Based Reasoning
- Paradox
- Darwin
- FINDER
- DCTP
- SATCHMO
- SCOTT
- Mace4
- iProver-Eq
- iProver
- MGTP
- YAGO
- CLIN
- E-KRHyper
- Geo 2007F
- ModGen
- Peers-mcd
- margrave
- GeoNames
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- CPSA
- Theorem proving for classical logic with partial functions by reduction to Kleene logic
- Finite reasons for safety. Parameterized verification by finite model finding
- Razor
- 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
