The use of embeddings to provide a clean separation of term and annotation for higher order rippling
From MaRDI portal
Publication:540694
DOI10.1007/s10817-010-9177-yzbMath1216.68232OpenAlexW1971433298MaRDI QIDQ540694
Alan Smaill, Ian Green, Louise Abigail Dennis
Publication date: 3 June 2011
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9177-y
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rippling: A heuristic for guiding inductive proofs
- Isabelle. A generic theorem prover
- Managing structural information by higher-order colored unification
- Productive use of failure in inductive proof
- A calculus for and termination of rippling
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Theorem Proving in Higher Order Logics