To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

How to transfigure the Wikipedia

Would you like Wikipedia to always look as professional and up-to-date? We have created a browser extension. It will enhance any encyclopedic page you visit with the magic of the WIKI 2 technology.

Try it — you can delete it anytime.

Install in 5 seconds
4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
Great Wikipedia has got greater.
.
Leo
Newton
Brights
Milds

Matita

From Wikipedia, the free encyclopedia

For the river in Romania, see Matița. For the Romanian village Matița, see Păcureți.
Matita
Developer(s)Matita team
Initial release1999
Written inOCaml
Operating systemLinux
Available inEnglish
TypeTheorem proving
LicenseGPL
Websitehttp://matita.cs.unibo.it at the Wayback Machine (archived 2023-02-04)

Matita[1] is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man–machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist.

Matita is based on a dependent type system known as the calculus of (co)inductive constructions (a derivative of the calculus of constructions), and is compatible, to some extent, with Coq.

The word "matita" means "pencil" in Italian (a simple and widespread editing tool). It is a reasonably small and simple application,[2] whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions. Matita adopts a tactic-based editing mode; (XML-encoded) proof objects are produced for storage and exchange.

YouTube Encyclopedic

  • 1/3
    Views:
    30 830
    3 961 545
    5 039
  • AI for Architects?
  • What Should You Major In?
  • De Morgan’s Laws #Shorts #math #computerscience #education

Transcription

Main features

Existential variables are native in Matita, allowing a simpler management of dependent goals.[3]

Matita implements a bidirectional type inference algorithm[4] exploiting both inferred and expected types.

The power of the type inference system (refiner) is further augmented by a mechanism of hints[5] that helps in synthesizing unifiers in particular situations specified by the user.

Matita supports a sophisticated disambiguation strategy[6] based on a dialog between the parser and the typechecker.

At the interactive level, the system implements a small step execution of structured tactics[7] allowing a much better management of the proof development, and naturally leading to more structured and readable scripts.

Applications

Matita has been employed in CerCo (Certified Complexity): a FP7 European Project focused on the development of a formally verified, complexity preserving compiler from a large subset of C to the assembly language of a MCS-51 microprocessor.

Documentation

The Matita tutorial[8] provides a pragmatic introduction to the main functionalities of the Matita interactive theorem prover, offering a guided tour through a set of non-trivial examples in the field of software specification and verification.

See also

References

  1. ^ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. "The Matita Interactive Theorem Prover": CADE-23, LNCS 6803, 2011, pp. 64-69.
  2. ^ Asperti, A.; Ricciotti, W.; Sacerdoti Coen, C.; Tassi, E. (2009). "A compact kernel for the calculus of inductive constructions". Sādhanā. 34: 71–144. doi:10.1007/s12046-009-0003-3.
  3. ^ Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "A new type for tactics": Technical Report UBLCS-2009-14. June 2009.
  4. ^ Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions" Logical Methods in Computer Science, V.8, n. 1
  5. ^ Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "Hints in unification": LNCS V.5674, 2009, pp 84-98
  6. ^ Claudio Sacerdoti Coen, Stefano Zacchiroli "Efficient Ambiguous Parsing of Mathematical Formulae" LNCS V.3119, 2004, pp 347-362 
  7. ^ Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli "Tinycals: Step by Step Tacticals" ENTCS V.174, n.2, 2007, Pages 125–142
  8. ^ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen "Matita Tutorial" Journal of Formalized Reasoning, V.7, n. 2, 2014, Pages 91-199

External links

This page was last edited on 10 April 2024, at 00:52
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.
Contact WIKI 2
Introduction
Terms of Service
Privacy Policy