SPIKE
From MaRDI portal
swMATH10186MaRDI QIDQ22153FDOQ22153
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/BFb0013087
Cited In (32)
- 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?)
- Narrowing based inductive proof search
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Combining superposition and induction: a practical realization
- Proving termination by dependency pairs and inductive theorem proving
- Decidability and undecidability results for propositional schemata
- Implicit induction in conditional theories
- Rewriting of imperative programs into logical equations
- Termination of constructor systems
- NQTHM
- Termination of theorem proving by reuse
- InKa
- A3PAT
- EXPANDER
- VeriFun
- QuodLibet
- REVE
- RRL
- UNICOM
- Inductive proof search modulo
- Completeness and decidability results for first-order clauses with indices
- Perfect discrimination graphs: indexing terms with integer exponents
- Title not available (Why is that?)
- 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
