A Mizar mode for HOL
From MaRDI portal
Publication:6567713
DOI10.1007/bfb0105406zbMath1543.68402MaRDI QIDQ6567713
Publication date: 5 July 2024
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A higher-order implementation of rewriting
- Set theory in first-order logic: Clauses for Gödel's axioms
- Obvious inferences
- A deficiency of natural deduction
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- On the shape of mathematical arguments
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Automated deduction -- CADE-12. 12th international conference, Nancy, France, June 26 -- July 1, 1994. Proceedings
- Isabelle. A generic theorem prover
- Edinburgh LCF. A mechanized logic of computation
- lean\(T^ AP\): Lean tableau-based deduction
- Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
- Optimizing proof search in model elimination
- An examination of the prolog technology theorem-prover
- Minimizing the number of clauses by renaming
This page was built for publication: A Mizar mode for HOL
