Higher-order annotated terms for proof search

DOI10.1007/bfb0105418zbMATH Open1543.68412MaRDI QIDQ6567727

Ian Green, Alan Smaill

Publication date: 5 July 2024

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Challenge problems in elementary calculus
• Implementing tactics and tacticals in a higher-order logic programming language
• A framework for defining logics
• Natural deduction as higher-order resolution
• About the theory of tree embedding
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Termination orderings for rippling
• The OYSTER-CLAM system

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