Higher-order annotated terms for proof search

DOI10.1007/BFB0105418MaRDI QIDQ6567727zbMATH OpenFDO

Authors Alan Smaill, Ian Green

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105418

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• Managing structural information by higher-order colored unification
• A colored version of the -calculus
• A calculus for and termination of rippling
• Rippling: Meta-Level Guidance for Mathematical Reasoning

Cites work

• A framework for defining logics
• A logic programming language with lambda-abstraction, function variables, and simple unification
• About the theory of tree embedding
• Challenge problems in elementary calculus
• scientific article; zbMATH DE number 3961577 (Why is no real title available?)
• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• Implementing tactics and tacticals in a higher-order logic programming language
• Natural deduction as higher-order resolution
• Rippling: A heuristic for guiding inductive proofs
• Termination orderings for rippling
• The OYSTER-CLAM system

This page was built for publication: Higher-order annotated terms for proof search

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