Cited in
(46)- Blocking and other enhancements for bottom-up model generation methods
- 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
- Deciding effectively propositional logic using DPLL and substitution sets
- Computing finite models by reduction to function-free clause logic
- Rule-based static analysis of network protocol implementations
- Paradox
- FINDER
- DCTP
- SATCHMO
- E-Darvin
- Mace4
- iProver-Eq
- Equinox
- iProver
- MGTP
- YAGO
- CLIN
- E-KRHyper
- Geo 2007F
- ModGen
- Denali
- margrave
- GeoNames
- CPSA
- Razor
- Model Representation over Finite and Infinite Signatures
- Automated reasoning building blocks
- Model evolution with equality -- revised and implemented
- Automated Deduction – CADE-20
- Theorem proving for classical logic with partial functions by reduction to Kleene logic
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- MACE4 and SEM: a comparison of finite model generators
- The model evolution calculus as a first-order DPLL method
- Exploiting symmetry in SMT problems
- Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention
- Model finding for recursive functions in SMT
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- Constraint solving for finite model finding in SMT solvers
This page was built for software: Darwin
