Managing structural information by higher-order colored unification

DOI10.1023/A:1006282725324MaRDI QIDQ1582389zbMATHOpenAlexWikidataFDO

Authors Dieter Hutter, Michael Kohlhase

Publication date 3 October 2000

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1006282725324

zbMATH Keywords

ripplinghigher-order unificationinductive theorem provingformalization of coloring termssimply typed \(\lambda\) calculus with color annotations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• A colored version of the \(\lambda\)-calculus
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• A calculus for and termination of rippling
• Rippling: A heuristic for guiding inductive proofs
• Rippling: Meta-Level Guidance for Mathematical Reasoning

Cited in

(3)

• A colored version of the \(\lambda\)-calculus
• Higher-order annotated terms for proof search
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling

This page was built for publication: Managing structural information by higher-order colored unification

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