The following pages link to Christoph Weidenbach (Q831914):
Displaying 50 items.
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Labelled splitting (Q1037396) (← links)
- Unification in sort theories and its applications (Q1380412) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- New techniques for linear arithmetic: cubes and equalities (Q1688532) (← links)
- A note on assumptions about Skolem functions (Q1904405) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- Superposition decides the first-order logic fragment over ground theories (Q1949088) (← links)
- Generalized completeness for SOS resolution and its application to a new notion of relevance (Q2055868) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- An efficient subsumption test pipeline for BS(LRA) clauses (Q2104505) (← links)
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL (Q2104508) (← links)
- Semantic relevance (Q2104509) (← links)
- SCL(EQ): SCL for first-order logic with equality (Q2104511) (← links)
- On the expressivity and applicability of model representation formalisms (Q2180214) (← links)
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories (Q2234101) (← links)
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) (← links)
- SPASS-SATT. A CDCL(LA) solver (Q2305409) (← links)
- SCL clause learning from simple models (Q2305416) (← links)
- A complete and terminating approach to linear integer solving (Q2307624) (← links)
- On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic (Q2405242) (← links)
- Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints (Q2405251) (← links)
- Computing small clause normal forms (Q2751358) (← links)
- Combining superposition, sorts and splitting (Q2751379) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Fast Cube Tests for LIA Constraint Solving (Q2817914) (← links)
- Automatic Generation of Invariants for Circular Derivations in SUP(LA) (Q2891451) (← links)
- Labelled Superposition for PLTL (Q2891470) (← links)
- Combination of Disjoint Theories: Beyond Decidability (Q2908497) (← links)
- A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance (Q2908524) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Superposition for fixed domains (Q2946615) (← links)
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Q2964454) (← links)
- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation (Q2964455) (← links)
- BDI: a new decidable clause class (Q2987061) (← links)
- First-Order Atom Definitions Extended (Q2996171) (← links)
- Superposition Modulo Non-linear Arithmetic (Q3172887) (← links)
- Automated Reasoning Building Blocks (Q3449631) (← links)
- Linear Integer Arithmetic Revisited (Q3454126) (← links)
- Superposition for Fixed Domains (Q3540186) (← links)
- Labelled Splitting (Q3541723) (← links)
- Subterm contextual rewriting (Q3568223) (← links)
- Labelled Clauses (Q3608781) (← links)
- System Description: Spass Version 3.0 (Q3608799) (← links)
- Deciding the Inductive Validity of ∀ ∃ * Queries (Q3644758) (← links)
- Superposition Modulo Linear Arithmetic SUP(LA) (Q3655193) (← links)
- (Q3838762) (← links)
- (Q4249904) (← links)
- (Q4261067) (← links)
- (Q4263167) (← links)
