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 72 articles , 3 standard articles )

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

1 2 3 4 next

  1. Hammachukiattikul, Porpattama; Mohanapriya, Arusamy; Ganesh, Anumanthappa; Rajchakit, Grienggrai; Govindan, Vediyappan; Gunasekaran, Nallappan; Lim, Chee Peng: A study on fractional differential equations using the fractional Fourier transform (2020)
  2. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  3. Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico: Implementing type theory in higher order constraint logic programming (2019)
  4. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  5. Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio: The Coq library as a theory graph (2019)
  6. Sacerdoti Coen, Claudio: A plugin to export Coq libraries to XML (2019)
  7. Paolini, Luca; Piccolo, Mauro; Roversi, Luca: A certified study of a reversible programming language (2018)
  8. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  9. Maietti, Maria Emilia: On choice rules in dependent type theory (2017)
  10. Blanqui, Frédéric: Termination of rewrite relations on (\lambda)-terms based on Girard’s notion of reducibility (2016)
  11. Calude, Cristian S.; Thompson, Declan: Incompleteness, undecidability and automated proofs (invited talk) (2016)
  12. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definitions in higher-order logic (2016)
  13. Selsam, Daniel; de Moura, Leonardo: Congruence closure in intensional type theory (2016)
  14. Asperti, Andrea: Reverse complexity (2015)
  15. Asperti, Andrea: Computational complexity via finite types (2015)
  16. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  17. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Foundational extensible corecursion: a proof assistant perspective (2015)
  18. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  19. Fridlender, Daniel; Pagano, Miguel: Pure type systems with explicit substitutions (2015)
  20. Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding Kleene algebra terms equivalence in Coq (2015)

1 2 3 4 next