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

DOI10.1007/S10817-010-9177-YMaRDI QIDQ540694zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

automated theorem provinghigher order logicproof planningrippling

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 1696789 (Why is no real title available?)
• scientific article; zbMATH DE number 176755 (Why is no real title available?)
• scientific article; zbMATH DE number 1348457 (Why is no real title available?)
• scientific article; zbMATH DE number 1863385 (Why is no real title available?)
• A calculus for and termination of rippling
• Isabelle. A generic theorem prover
• Managing structural information by higher-order colored unification
• Productive use of failure in inductive proof
• Rippling: A heuristic for guiding inductive proofs
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Theorem Proving in Higher Order Logics

Cited in

(4)

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

Describes a project that uses

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)