Automating Most Parts of Hardware Proofs in HOL
No abstract available.
Related papers
- Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP 2016
- A Lambda-Superposition Tactic for Isabelle/HOL CPP 2026
- Premise Selection and External Provers for HOL4 CPP 2015
- Certified Connection Tableaux Proofs for HOL Light and TPTP CPP 2015
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) CPP 2019
- Balancing Automation and Control for Formal Verification of Microprocessors CAV 2021
- Proofs as Programs TOPLAS 1985
- An extension of the framework types-to-sets for Isabelle/HOL CPP 2022