Hybrid interactive theorem proving using nuprl and HOL

DOI10.1007/3-540-63104-6_34zbMath1430.68403OpenAlexW1592271195MaRDI QIDQ5234717

Douglas J. Howe, Amy P. Felty

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_34

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Innovations in computational type theory using Nuprl

Uses Software

• Coq
• Isabelle
• ML
• PVS
• HOL
• Nuprl
• NQTHM
• HOL90

Cites Work

• Isabelle. A generic theorem prover
• Edinburgh LCF. A mechanized logic of computation
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Cache coherency in SCI: Specification and a sketch of correctness
• Unnamed Item
• Unnamed Item
• Unnamed Item