Darwin

swMATH4175MaRDI QIDQ16359FDOQ16359

Author name not available (Why is that?)

Cited In (26)

• 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
• 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
• 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
• Model Representation over Finite and Infinite Signatures
• Automated reasoning building blocks
• Automated Deduction – CADE-20
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Theorem proving for classical logic with partial functions by reduction to Kleene logic
• Model evolution with equality -- revised and implemented
• 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