Managing structural information by higher-order colored unification

DOI10.1023/A:1006282725324zbMATH Open0959.03007OpenAlexW1602983059WikidataQ57389430 ScholiaQ57389430MaRDI QIDQ1582389FDOQ1582389

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

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

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)

Cited In (3)

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

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)