swMATH6140MaRDI QIDQ18274FDOQ18274
Author name not available (Why is that?)
Official website: http://matita.cs.unibo.it/
Cited In (only showing first 100 items - show all)
- 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
- The strategy challenge in SMT solving
- Towards semantic mathematical editing
- Dot-types and their implementation
- Pure type systems with explicit substitutions
- Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
- Asynchronous user interaction and tool integration in Isabelle/PIDE
- Declarative representation of proof terms
- Crystal: Integrating structured queries into a tactic language
- Procedural representation of CIC proof terms
- Title not available (Why is that?)
- Incompleteness, Undecidability and Automated Proofs
- Validating Mathematical Structures
- Implementing type theory in higher order constraint logic programming
- Title not available (Why is that?)
- Zooid
- An Interactive Driver for Goal-directed Proof Strategies
- A study on fractional differential equations using the fractional Fourier transform
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
- 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
This page was built for software: Matita
