The Matita Interactive Theorem Prover

DOI10.1007/978-3-642-22438-6_7zbMath1341.68179OpenAlexW2166662837MaRDI QIDQ5200015

Enrico Tassi, Wilmer Ricciotti, Andrea Asperti, Claudio Sacerdoti Coen

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.232.3171

Mathematics Subject Classification ID

Related Items (21)

Reverse complexity ⋮ Validating Mathematical Structures ⋮ The Lean Theorem Prover (System Description) ⋮ Programming and Proving with Classical Types ⋮ Computational Complexity Via Finite Types ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Unnamed Item ⋮ Pure type systems with explicit substitutions ⋮ From types to sets by local type definition in higher-order logic ⋮ Friends with Benefits ⋮ On Choice Rules in Dependent Type Theory ⋮ Recycling proof patterns in Coq: case studies ⋮ The Strategy Challenge in SMT Solving ⋮ A formalization of multi-tape Turing machines ⋮ Congruence Closure in Intensional Type Theory ⋮ Matita ⋮ Natural Deduction Environment for Matita ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Implementing type theory in higher order constraint logic programming ⋮ A Certified Study of a Reversible Programming Language ⋮ Deciding Kleene algebra terms equivalence in Coq

Uses Software

• Coq
• OTTER
• Metis_
• Isar
• Mizar
• Proof General
• iProver
• CtCoq
• PoplMark
• Whelp

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automation for interactive proof: first prototype
• User interaction with the Matita proof assistant
• Declarative representation of proof terms
• Tinycals: Step by Step Tacticals
• Hints in Unification
• Working with Mathematical Structures in Type Theory
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• First-Class Type Classes
• The CADE-22 automated theorem proving system competition – CASC-22
• Smart Matching
• Subset Coercions in Coq
• About the Formalization of Some Results by Chebyshev in Number Theory
• Coercive subtyping
• An Interactive Driver for Goal-directed Proof Strategies
• Mathematical Knowledge Management
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs

This page was built for publication: The Matita Interactive Theorem Prover