The following pages link to Nicolas Peltier (Q167063):
Displaying 50 items.
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619) (← links)
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- Simplified handling of iterated term schemata (Q616760) (← links)
- (Q861366) (redirect page) (← links)
- Representing and building models for decidable subclasses of equational clausal logic (Q861367) (← links)
- Some techniques for proving termination of the hyperresolution calculus (Q861692) (← links)
- Constructing infinite models represented by tree automata (Q1044230) (← links)
- Increasing model building capabilities by constraint solving on terms with integer exponents (Q1360965) (← links)
- A new technique for verifying and correcting logic programs (Q1373300) (← links)
- Semantic generalizations for proving and disproving conjectures by analogy (Q1382153) (← links)
- Extracting models from clause sets saturated under semantic refinements of the resolution rule. (Q1401929) (← links)
- Model building with ordered resolution: Extracting models from saturated clause sets (Q1404975) (← links)
- A calculus combining resolution and enumeration for building finite models (Q1404976) (← links)
- A tableaux calculus for reducing proof size (Q1799068) (← links)
- A generic framework for implicate generation modulo theories (Q1799090) (← links)
- Superposition with datatypes and codatatypes (Q1799098) (← links)
- The first order theory of primal grammars is decidable (Q1882903) (← links)
- Modular instantiation schemes (Q1944184) (← links)
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (Q1984795) (← links)
- A superposition calculus for abductive reasoning (Q2013317) (← links)
- Unifying decidable entailments in separation logic with inductive definitions (Q2055854) (← links)
- Ilinva: using abduction to generate loop invariants (Q2180218) (← links)
- Prenex separation logic with one selector field (Q2180532) (← links)
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules (Q2234797) (← links)
- The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains (Q2289076) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- A complete superposition calculus for primal grammars (Q2352496) (← links)
- The binomial pricing model in finance: a formalization in Isabelle (Q2405273) (← links)
- Extended resolution simulates binary decision diagrams (Q2478427) (← links)
- Automated model building (Q2487870) (← links)
- On the decidability of the PVD class with equality (Q2743641) (← links)
- Reasoning on Schemas of Formulas: An Automata-Based Approach (Q2799178) (← links)
- A resolution calculus for first-order schemata (Q2843818) (← links)
- Combining Superposition and Induction: A Practical Realization (Q2849478) (← links)
- Schemata of Formulæ in the Theory of Arrays (Q2851948) (← links)
- Reasoning on Schemata of Formulæ (Q2907331) (← links)
- A Calculus for Generating Ground Explanations (Q2908490) (← links)
- Instantiation Schemes for Nested Theories (Q2946696) (← links)
- A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules (Q2987065) (← links)
- Decidability and Undecidability Results for Propositional Schemata (Q2996912) (← links)
- Schemata of SMT-Problems (Q3010358) (← links)
- A Rewriting Strategy to Generate Prime Implicates in Equational Logic (Q3192186) (← links)
- (Q3372480) (← links)
- Bottom-up Construction of Semantic Tableaux (Q3406692) (← links)
- Quantifier-Free Equational Logic and Prime Implicate Generation (Q3454103) (← links)
- A Needed Rewriting Strategy for Data-Structures with Pointers (Q3522009) (← links)
- Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview (Q3537540) (← links)
- Narrowing Data-Structures with Pointers (Q3541950) (← links)
- Complexity of the Satisfiability Problem for a Class of Propositional Schemata (Q3564849) (← links)
- I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness (Q3582694) (← links)
