scientific article; zbMATH DE number 7178361

zbMath1431.68125MaRDI QIDQ5219926

Makarius Wenzel

Publication date: 9 March 2020

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

On definitions of constants and types in HOL ⋮ Verified interactive computation of definite integrals ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL

Uses Software

• ACL2
• Coq
• Isabelle
• Nitpick
• Isabelle/HOL
• Isabelle/Isar
• PVS
• Metis_
• Mizar
• z3
• Proof General
• HOL
• OCaml
• PIDE
• Isabelle/jEdit
• HOL Light
• Sledgehammer
• LCF
• CakeML
• Coq/SSReflect
• CompCert
• Flyspeck
• Archive Formal Proofs

This page was built for publication: