Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5464664
DOI10.1007/b100400zbMath1099.68723OpenAlexW2798038182MaRDI QIDQ5464664
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (10)
A proof-centric approach to mathematical assistants ⋮ Conjecture synthesis for inductive theories ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ Integrating Maude into Hets ⋮ Integer induction in saturation ⋮ Induction in saturation-based proof search ⋮ Hipster: Integrating Theory Exploration in a Proof Assistant ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Uses Software
This page was built for publication: Theorem Proving in Higher Order Logics
