User interaction with the Matita proof assistant

DOI10.1007/s10817-007-9070-5zbMath1132.68673OpenAlexW2136219937WikidataQ56901952 ScholiaQ56901952MaRDI QIDQ2462635

Andrea Asperti, Stefano Zacchiroli, Claudio Sacerdoti Coen, Enrico Tassi

Publication date: 3 December 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-007-9070-5

zbMATH Keywords

XMLInteractive theorem provingAuthoringDigital librariesMathematical knowledge managementProof assistant

Mathematics Subject Classification ID

Related Items (18)

Declarative representation of proof terms ⋮ Procedural representation of CIC proof terms ⋮ Crystal: Integrating structured queries into a tactic language ⋮ Tactics for hierarchical proof ⋮ Certifying expressive power and algorithms of reversible primitive permutations with \textsf{Lean} ⋮ Formal metatheory of programming languages in the Matita interactive theorem prover ⋮ A User Interface for a Mathematical System that Allows Ambiguous Formulae ⋮ An Interactive Driver for Goal-directed Proof Strategies ⋮ A User-friendly Interface for a Lightweight Verification System ⋮ Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit ⋮ The Matita Interactive Theorem Prover ⋮ Isabelle as Document-Oriented Proof Assistant ⋮ Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita ⋮ Matita ⋮ Formalising Overlap Algebras in Matita ⋮ Type classes for mathematics in type theory ⋮ Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean} ⋮ Towards semantic mathematical editing

Uses Software

• Theorema
• OTTER
• Mizar
• Proof General
• Nuprl
• C-CoRN
• MML
• CtCoq
• HR
• Whelp

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Edinburgh LCF. A mechanized logic of computation
• Mathematical knowledge management in HELM
• A refinement of de Bruijn's formal language of mathematics
• Tinycals: Step by Step Tacticals
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• Coercive subtyping
• On the Structure of Mizar Types
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• From Notation to Semantics: There and Back Again
• Types for Proofs and Programs

This page was built for publication: User interaction with the Matita proof assistant