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
• Model Finding for Recursive Functions in SMT
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Title not available (Why is that?)
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Semantically-guided goal-sensitive reasoning: model representation
• Lemma Learning in the Model Evolution Calculus
• MACE4 and SEM: A Comparison of Finite Model Generators
• Deciding effectively propositional logic using DPLL and substitution sets
• Computing finite models by reduction to function-free clause logic
• Exploiting Symmetry in SMT Problems
• Rule-based static analysis of network protocol implementations
• Model Representation over Finite and Infinite Signatures
• Automated Deduction – CADE-20
• Theorem proving for classical logic with partial functions by reduction to Kleene logic
• Model evolution with equality -- revised and implemented
• Exploring Theories with a Model-Finding Assistant
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• The model evolution calculus as a first-order DPLL method
• Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention
• NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
• Superposition for Bounded Domains
• Automated Reasoning Building Blocks
• Constraint solving for finite model finding in SMT solvers

This page was built for software: Darwin