Matita

swMATH6140MaRDI QIDQ18274FDOQ18274

Author name not available (Why is that?)

Official website: http://matita.cs.unibo.it/

Described by source

• User interaction with the Matita proof assistant
• Matita Tutorial
• The Matita interactive theorem prover

Cited In (only showing first 100 items - show all)

• Type classes for efficient exact real arithmetic in \textsc{Coq}
• Hints in Unification
• From types to sets by local type definition in higher-order logic
• A certified study of a reversible programming language
• From types to sets by local type definitions in higher-order logic
• Towards ``mouldable code via nested code graph transformation
• Spurious disambiguation errors and how to get rid of them
• Superposition as a logical glue
• Type classes for mathematics in type theory
• About the Formalization of Some Results by Chebyshev in Number Theory
• Aligning concepts across proof assistant libraries
• Title not available (Why is that?)
• Title not available (Why is that?)
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
• Reverse complexity
• Computational Complexity Via Finite Types
• A formalization of multi-tape Turing machines
• Formalising overlap algebras in Matita
• A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita
• A canonical locally named representation of binding
• foaf
• LAD
• Proof General
• GtkMathView
• TeXmacs
• jsMath
• HOL-Omega
• C-CoRN
• A Compact Proof of Decidability for Regular Expression Equivalence
• NNexus
• Title not available (Why is that?)
• A Language of Patterns for Subterm Selection
• Polar
• STEX+
• KAT-ML
• Formulator MathML
• Coq/SSReflect
• Agda
• Epigram
• Irdis
• Proof General Kit
• CtCoq
• ProofWeb
• GUItar
• PDCoq
• Paco
• RATH-Agda
• CLPGUI
• Lean
• HOL Zero
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Congruence closure in intensional type theory
• The CADE-22 automated theorem proving system competition -- CASC-22
• Isabelle as document-oriented proof assistant
• Menhir
• Preface to the special issue: Interactive theorem proving and the formalization of mathematics
• CoqMTU
• Plat-Omega
• Theseus
• NetSketch
• scunac
• CoCaml
• Oz Explorer
• RedPRL
• HOLCF
• ELPI
• APT
• Heq
• Whelp
• cart-cube
• A formal proof of Borodin-Trakhtenbrot's gap theorem
• Tinycals: step by step tacticals
• Recycling proof patterns in Coq: case studies
• Tactics for hierarchical proof
• Packaging Mathematical Structures
• finmap
• PCM library
• Deciding Kleene algebra terms equivalence in Coq
• Formal metatheory of programming languages in the Matita interactive theorem prover
• Crafting a Proof Assistant
• A plugin to export Coq libraries to XML
• The Coq library as a theory graph
• Foundational extensible corecursion: a proof assistant perspective
• A Web Interface for Matita
• Formalizing Turing Machines
• Proviola: a tool for proof re-animation
• The Lean theorem prover (system description)
• Friends with benefits. Implementing corecursion in foundational proof assistants
• A bi-directional refinement algorithm for the calculus of (co)inductive constructions
• A user-friendly interface for a lightweight verification system
• The swap of integral and limit in constructive mathematics
• Programming and Proving with Classical Types
• From the universality of mathematical truth to the interoperability of proof systems
• Enabling collaboration on semiformal mathematical knowledge by semantic web integration
• On choice rules in dependent type theory
• Natural Deduction Environment for Matita
• A user interface for a mathematical system that allows ambiguous formulae
• Formalization of formal topology by means of the interactive theorem prover Matita
• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit

This page was built for software: Matita