The following pages link to InKa (Q31435):
Displaying 20 items.
- A recursion planning analysis of inductive completion (Q1353935) (← links)
- Superposition with structural induction (Q1687553) (← links)
- On terminating lemma speculations. (Q1854370) (← links)
- Induction using term orders (Q1915132) (← links)
- Middle-out reasoning for synthesis and induction (Q1915136) (← links)
- A calculus for and termination of rippling (Q1915137) (← links)
- Proving theorems by reuse (Q1978233) (← links)
- Induction and Skolemization in saturation theorem proving (Q2084957) (← links)
- Sound lemma generation for proving inductive validity of equations (Q3165943) (← links)
- (Q4264710) (← links)
- (Q4524769) (← links)
- Termination of algorithms over non-freely generated data types (Q4647505) (← links)
- INKA: The next generation (Q4647524) (← links)
- Termination of constructor systems (Q5055852) (← links)
- Synthesis of induction orderings for existence proofs (Q5210760) (← links)
- Induction using term orderings (Q5210765) (← links)
- Plagiator — A learning prover (Q5234707) (← links)
- Reasoning About Incompletely Defined Programs (Q5387856) (← links)
- Mathematical Knowledge Management (Q5898516) (← links)
- MBase: Representing knowledge and context for the integration of mathematical software systems (Q5950933) (← links)
