A user-friendly interface for a lightweight verification system

DOI10.1016/J.ENTCS.2012.06.004MaRDI QIDQ5170234zbMATH OpenOpenAlexWikidataFDO

Authors Andrei Lapets, Assaf Kfoury

Publication date 22 July 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2012.06.004

zbMATH Keywords

formal verificationuser interfaces

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Recommendations

• Supporting the formal verification of mathematical texts
• User interaction with the Matita proof assistant
• A user interface for a mathematical system that allows ambiguous formulae
• A graphical user interface for formal proofs in geometry
• Automated Reasoning

Cites work

• A computer environment for writing ordinary mathematical proofs
• Computerizing mathematical text with MathLang
• scientific article; zbMATH DE number 1696759 (Why is no real title available?)
• scientific article; zbMATH DE number 1951639 (Why is no real title available?)
• scientific article; zbMATH DE number 1980938 (Why is no real title available?)
• scientific article; zbMATH DE number 1497860 (Why is no real title available?)
• Integrating searching and authoring in Mizar
• Isabelle. A generic theorem prover
• Mechanizing Mathematical Reasoning
• On Correctness of Mathematical Texts from a Logical and Practical Point of View
• Safe compositional network sketches: formal framework
• User interaction with the Matita proof assistant
• Verifying and Invalidating Textbook Proofs Using Scunak
• Verifying programs in the calculus of inductive constructions
• Web interfaces for proof assistants

Describes a project that uses

Uses Software

• PVS
• Fortress
• NetSketch
• Isabelle
• Mizar
• scunac
• Matita

This page was built for publication: A user-friendly interface for a lightweight verification system

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