Hybrid interactive theorem proving using Nuprl and HOL

DOI10.1007/3-540-63104-6_34MaRDI QIDQ5234717zbMATH OpenOpenAlexFDO

Authors Amy P. Felty, Douglas J. Howe

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

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

Recommendations

• scientific article; zbMATH DE number 1863394
• scientific article; zbMATH DE number 3986665
• Toward sharing libraries of mathematics between theorem provers
• scientific article; zbMATH DE number 1113859
• TPS: A hybrid automatic-interactive system for developing proofs

Cites work

• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Cache coherency in SCI: Specification and a sketch of correctness
• Edinburgh LCF. A mechanized logic of computation
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 1113859 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Isabelle. A generic theorem prover

Cited in

(6)

• A synthesis of the procedural and declarative styles of interactive theorem proving
• scientific article; zbMATH DE number 3986665 (Why is no real title available?)
• scientific article; zbMATH DE number 1113859 (Why is no real title available?)
• scientific article; zbMATH DE number 1863394 (Why is no real title available?)
• Importing mathematics from HOL into Nuprl
• Innovations in computational type theory using Nuprl

Describes a project that uses

Uses Software

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

This page was built for publication: Hybrid interactive theorem proving using Nuprl and HOL

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