SPIKE
From MaRDI portal
Software:22153
swMATH10186MaRDI QIDQ22153FDOQ22153
Author name not available (Why is that?)
Cited In (23)
- On terminating lemma speculations.
- Proof search and proof check for equational and inductive theorems.
- A Schemata Calculus for Propositional Logic
- Title not available (Why is that?)
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Proving termination by dependency pairs and inductive theorem proving
- Completeness and Decidability Results for First-Order Clauses with Indices
- Implicit induction in conditional theories
- Perfect Discrimination Graphs: Indexing Terms with Integer Exponents
- Rewriting of imperative programs into logical equations
- Combining Superposition and Induction: A Practical Realization
- Termination of constructor systems
- Termination of theorem proving by reuse
- Inductive proof search modulo
- Decidability and Undecidability Results for Propositional Schemata
- Title not available (Why is that?)
- Narrowing Based Inductive Proof Search
- Strategic issues, problems and challenges in inductive theorem proving
- Mechanically certifying formula-based Noetherian induction reasoning
- Proving theorems by reuse
- A general framework to build contextual cover set induction provers
- Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps
- Combining induction and saturation-based theorem proving
This page was built for software: SPIKE
