A formal proof generator from semi-formal proof documents

DOI10.1007/978-3-319-67729-3_1MaRDI QIDQ1675786zbMATH OpenOpenAlexFDO

Authors Adrián Riesco, Kazuhiro Ogata

Publication date 3 November 2017

Full work available at URL https://doi.org/10.1007/978-3-319-67729-3_1

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Generic proof scores for generate \& check method in CafeOBJ
• scientific article; zbMATH DE number 1629953
• scientific article; zbMATH DE number 1104364
• scientific article; zbMATH DE number 1140678
• Mathematical Knowledge Management

Cited in

(3)

• CiMPA
• CiMPG
• scientific article; zbMATH DE number 6938205 (Why is no real title available?)

Describes a project that uses

Uses Software

• CafeOBJ
• Maude
• Hets
• CafeInMaude
• Dafny
• Isabelle/HOL
• PVS
• LARCH

This page was built for publication: A formal proof generator from semi-formal proof documents

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