SPIKE
From MaRDI portal
Cited in
(33)- Inductive proof search modulo
- PLAGIATOR
- On terminating lemma speculations.
- Implicit induction in conditional theories
- NQTHM
- Proving theorems by reuse
- Combining induction and saturation-based theorem proving
- Rewriting of imperative programs into logical equations
- Strategic issues, problems and challenges in inductive theorem proving
- Combining superposition and induction: a practical realization
- Decidability and undecidability results for propositional schemata
- InKa
- A3PAT
- VeriFun
- EXPANDER
- Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps
- A Schemata Calculus for Propositional Logic
- QuodLibet
- UNICOM
- RRL
- REVE
- Proving termination by dependency pairs and inductive theorem proving
- scientific article; zbMATH DE number 1149426 (Why is no real title available?)
- scientific article; zbMATH DE number 2043539 (Why is no real title available?)
- Termination of theorem proving by reuse
- Narrowing based inductive proof search
- Completeness and decidability results for first-order clauses with indices
- Termination of constructor systems
- Mechanically certifying formula-based Noetherian induction reasoning
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Perfect discrimination graphs: indexing terms with integer exponents
- Proof search and proof check for equational and inductive theorems.
- A general framework to build contextual cover set induction provers
This page was built for software: SPIKE
