The use of embeddings to provide a clean separation of term and annotation for higher order rippling

DOI10.1007/S10817-010-9177-YzbMATH Open1216.68232OpenAlexW1971433298MaRDI QIDQ540694FDOQ540694

Authors: Louise A. Dennis, Ian Green, Alan Smaill 

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

Recommendations

• A calculus for and termination of rippling
• A colored version of the \(\lambda\)-calculus
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Rippling: A heuristic for guiding inductive proofs
• Managing structural information by higher-order colored unification

zbMATH Keywords

automated theorem provinghigher order logicproof planningrippling

Mathematics Subject Classification ID

Cites Work

• Isabelle. A generic theorem prover
• Productive use of failure in inductive proof
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Theorem Proving in Higher Order Logics
• Managing structural information by higher-order colored unification
• A calculus for and termination of rippling
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Rippling: A heuristic for guiding inductive proofs

Cited In (4)

• Higher-order annotated terms for proof search
• Theorem Proving in Higher Order Logics
• Managing structural information by higher-order colored unification
• A colored version of the \(\lambda\)-calculus

Uses Software

• Isabelle
• IsaPlanner
• LEGO
• Lambda-Clam

This page was built for publication: The use of embeddings to provide a clean separation of term and annotation for higher order rippling

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q540694)