Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna. An interactive prover is a software tool aiding the development of formal proofs by man-machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist, and an interactive environment keeping the current status of the proof, and updating it according to commands (usually called tactics) issued by the user.

References in zbMATH (referenced in 56 articles , 2 standard articles )

Showing results 1 to 20 of 56.
Sorted by year (citations)

1 2 3 next

  1. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  2. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  3. Maietti, Maria Emilia: On choice rules in dependent type theory (2017)
  4. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  5. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definitions in higher-order logic (2016)
  6. Selsam, Daniel; de Moura, Leonardo: Congruence closure in intensional type theory (2016)
  7. Asperti, Andrea: Reverse complexity (2015)
  8. Asperti, Andrea: Computational complexity via finite types (2015)
  9. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  10. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  11. Fridlender, Daniel; Pagano, Miguel: Pure type systems with explicit substitutions (2015)
  12. Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding Kleene algebra terms equivalence in Coq (2015)
  13. van der Hoeven, Joris: Towards semantic mathematical editing (2015)
  14. Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
  15. Kahl, Wolfram: Towards “mouldable code” via nested code graph transformation (2014)
  16. de Moura, Leonardo; Passmore, Grant Olney: The strategy challenge in SMT solving (2013)
  17. Krebbers, Robbert; Spitters, Bas: Type classes for efficient exact real arithmetic in Coq (2013)
  18. Asperti, Andrea: A compact proof of decidability for regular expression equivalence (2012)
  19. Asperti, Andrea; Ricciotti, Wilmer: A web interface for Matita (2012)
  20. Asperti, Andrea; Ricciotti, Wilmer: Formalizing Turing machines (2012)

1 2 3 next