Theorem Proving in Higher Order Logics

DOI10.1007/B100400MaRDI QIDQ5464664zbMATH OpenOpenAlexFDO

Authors Lucas Dixon, Jacques D. Fleuriot

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Recommendations

• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Rippling: A heuristic for guiding inductive proofs
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• Termination orderings for rippling
• A calculus for and termination of rippling

Cited in

(15)

• Integer induction in saturation
• Induction in saturation-based proof search
• Dynamic rippling, middle-out reasoning and lemma discovery
• Integrating Maude into Hets
• Conjecture synthesis for inductive theories
• scientific article; zbMATH DE number 1863385 (Why is no real title available?)
• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• Automated cyclic entailment proofs in separation logic
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Hipster: integrating theory exploration in a proof assistant
• Case-analysis for rippling and inductive proof
• Rippling: A heuristic for guiding inductive proofs
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
• A proof-centric approach to mathematical assistants

Describes a project that uses

Uses Software

• IsaPlanner

This page was built for publication: Theorem Proving in Higher Order Logics

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