The following pages link to Automated Deduction – CADE-19 (Q5900727):
Displaying 22 items.
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Model evolution and refinement (Q436356) (← links)
- A combined superposition and model evolution calculus (Q438531) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Comparing instance generation methods for automated reasoning (Q877884) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Deciding effectively propositional logic using DPLL and substitution sets (Q972432) (← links)
- Computing finite models by reduction to function-free clause logic (Q1006733) (← links)
- First order Stålmarck. Universal lemmas through branch merges (Q1040785) (← links)
- Eliminating models during model elimination (Q2142079) (← links)
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) (← links)
- The model evolution calculus as a first-order DPLL method (Q2389629) (← links)
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Q2964454) (← links)
- MACE4 and SEM: A Comparison of Finite Model Generators (Q4913862) (← links)
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning (Q4916080) (← links)
- The Relative Power of Semantics and Unification (Q4916085) (← links)
- First-Order Resolution Methods for Modal Logics (Q4916086) (← links)
- Superposition and Model Evolution Combined (Q5191094) (← links)
- Decidability Results for Saturation-Based Model Building (Q5191116) (← links)
- Model Evolution with Equality Modulo Built-in Theories (Q5200017) (← links)
- System Description: SPASS-FD (Q5200034) (← links)
- An Algorithm for Approximating the Satisfiability Problem of High-level Conditions (Q5403460) (← links)
