Matita

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.

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

Read other articles:

The New 52

DC Comics superhero comic books series The New 52Cover of DC Comics: The New 52 #1, July 2011Publication informationPublisherDC ComicsGenre Superhero Publication dateAugust 31, 2011 – May 25, 2016Main character(s)DC UniverseCreative teamWritten byVariousArtist(s)VariousCollected editionsDC Comics The New 52ISBN 978-1-4012-3451-5DC Comics The New 52 Zero OmnibusISBN 978-1-4012-3884-1DC Comics The New 52 Villains OmnibusISBN 978-1-4012-4496-5 The New 52 was the 2...

 

 

Alpha Doradus

Alpha Doradus Lokasi α Doradus (lingkaran)Data pengamatan Epoch J2000.0      Equinox J2000.0 (ICRS)Rasi bintangDoradoKomponenABAsensio rekta 04j 33m 04j 33m 59.778s59.782sDeklinasi −55° 02′[1] −55° 02′[2] 41.91″42.39″Magnitudo semu (V)3.8[3]4.3[3]KarakteristikKlasifikasi bintangA0IIIp[3]B9IV[3]U-B Indeks warna−0.35[3]B-V Indeks warna−0.10&...

 

 

List of mayors of Kolkata

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: List of mayors of Kolkata – news · newspapers · books · scholar · JSTOR (December 2017) (Learn how and when to remove this template message) Mayor of KolkataIncumbentFirhad Hakimsince 22 November 2018Kolkata Municipal CorporationStyleHonorable MayorMember...

Susanna White (Mayflower passenger)

Founding member of Plymouth Colony Susanna (Jackson) White Winslow (c. 1592-after 1654) was a passenger on the Mayflower and successively wife of fellow Mayflower passengers William White and Edward Winslow.[1][2] Born Susanna Jackson, the daughter of Richard and Mary (Pettinger) Jackson,[3][better source needed] she went to Amsterdam and joined its separatist congregation about 1608, and there she married future Mayflower passenger William Whit...

 

 

K. D. Sethna

Indian historian and writer K.D. SethnaBorn(1904-11-26)26 November 1904Died29 June 2011(2011-06-29) (aged 106)Sri Aurobindo Ashram, Pondicherry, IndiaPen nameAmal KiranOccupationPoet, scholar, writer, philosopher, and cultural criticNationalityIndian Sri Aurobindo Family Rajnarayan Basu (Maternal grandfather) Manmohan Ghose (Elder brother) Barin Ghosh (Younger brother) Krishna Kumar Mitra (Maternal uncle) Political career Anushilan Samiti Jugantar Partition of Bengal Alipore bomb case Ju...

 

 

Bennett Park (New York City)

Public park in Manhattan, New York For the former Detroit Tigers ballpark, see Bennett Park (Detroit). 40°51′10″N 73°56′17″W / 40.85278°N 73.93806°W / 40.85278; -73.93806 The highest natural point in Manhattan; in the inset is the stone marker seen in the lower right of the larger image. Plaque commemorating the site of Fort Washington; see the close up of the right-hand badge at the bottom of the plaque in this article's gallery of images Bennett Park, als...

Rio Grande (1950 film)

1950 film by John Ford Rio GrandeTheatrical posterDirected byJohn FordScreenplay byJames Kevin McGuinnessBased onMission With No Record1947 story Saturday Evening Postby James Warner BellahProduced byUncredited:Merian C. CooperJohn FordStarring John Wayne Maureen O'Hara CinematographyBert GlennonEdited byJack MurrayMusic byVictor YoungProductioncompanies Republic Pictures Argosy Pictures Distributed byRepublic PicturesRelease date November 15, 1950 (1950-11-15) Running time105 ...

 

 

Giannino Camperio

Giannino Camperio Nazionalità  Italia Calcio Ruolo Allenatore (ex Centrocampista) Termine carriera 1903 - giocatore1911 - allenatore Carriera Squadre di club1 1900 Milan0 (0)1902-1903 Milan0 (0) Carriera da allenatore 1908-1911 Milan1910-1911 ItaliaCom. tecnica 1 I due numeri indicano le presenze e le reti segnate, per le sole partite di campionato.Il simbolo → indica un trasferimento in prestito.   Modifica dati su Wikidata · Manuale Giannino Camperio, all'...

 

 

American Fiction (film)

American FictionPoster filmSutradaraCord JeffersonProduser Cord Jefferson Jermaine Johnson Nikos Karamigios Ben LeClair SkenarioCord JeffersonBerdasarkanErasureoleh Percival EverettPemeran Jeffrey Wright Tracee Ellis Ross John Ortiz Erika Alexander Leslie Uggams Adam Brody Keith David Issa Rae Sterling K. Brown Penata musikLaura KarpmanSinematograferCristina DunlapPenyuntingHilda RasulaPerusahaanproduksi Orion Pictures MRC Film T-Street Productions 3 Arts Entertainment DistributorMetro-...

عائلة جوسلر

هذه المقالة يتيمة إذ تصل إليها مقالات أخرى قليلة جدًا. فضلًا، ساعد بإضافة وصلة إليها في مقالات متعلقة بها. (أغسطس 2018)Learn how and when to remove this message عائلة جوسلر وتشمل فرع العائلة بيرنبرغ-جوسلر، هي عائلة فلمندية من الهانزيتين وعائلة مصرفية نبيلة مسقط رأسها من هامبورغ. تنحدر العائلة �...

 

 

Listed buildings in England

Incomplete list of listed buildings in England England within the United Kingdom This is an as yet incomplete list of listed buildings in England, which are the majority of the listed buildings of the United Kingdom. The organisation of the lists in this series is on the same basis as the statutory register. County names are those used in the register, broadly based on the ceremonial counties and not always matching the current administrative areas. Grade I listed buildings in England At the ...

 

 

حركات دينية جديدة

حركات دينية جديدةمعلومات عامةصنف فرعي من religious community (en) حركة دينية يدرسه دراسة العقائد الدينية ممثلة بـ religious syncretism (en) النقيض حركة معادية للطائفةtraditional religion (en) تعديل - تعديل مصدري - تعديل ويكي بيانات الحركات الدينية الجديدة هو مصطلح يشير إلى الجماعات والفرق الدينية التي ظهر...

عدد كسري

عدد كسريمعلومات عامةصنف فرعي من عدد قابل للإنشاءعدد حقيقيعدد تقاربي بتردد p جزء من مجموعة الأعداد الكسرية يدرسه rational number theory (en) تعريف الصيغة a b ∈ Q ⇔ a ∈ Z , b ∈ N {\displaystyle {\frac {a}{b}}\in \mathbb {Q} \Leftrightarrow a\in \mathbb {Z} ,b\in \mathbb {N} } الرموز في الصيغة Q {\displaystyle \mathbb {Q} } Z {\displaystyle \mathbb {Z}...

 

 

Amorepacific Corporation

South Korean beauty and cosmetics conglomerate Amorepacific CorporationNative name주식회사 아모레퍼시픽Traded asKRX: 090430IndustryCosmeticsPerfumeFounded5 September 1945; 78 years ago (1945-09-05) as Pacific Chemical Co. Ltd.FounderSuh Sung-whanHeadquartersYongsan-gu, Seoul, South KoreaKey peopleSuh Kyung-bae (Chairperson)Revenue KRW 4.78 trillion (2021)[1]Operating income KRW 379 billion (2021)[1]Net income KRW 267 billion (2021)[1]Total a...

 

 

Diet of Hungary

Parliament of the Kingdom of Hungary For the post-1946 institution, see National Assembly of Hungary. For the food of Hungary, see Hungarian cuisine. Diet of Hungary of 1830 This article is missing information about the Diet between 1918 and 1946. Please expand the article to include this information. Further details may exist on the talk page. (March 2024) The Diet of Hungary or originally: Parlamentum Publicum / Parlamentum Generale[1] (Hungarian: Országgyűlés) was the most impor...

1953 في السعودية

← 1952 1951 1950 1953 في السعودية → 1954 1955 1956 عقود: طالع أيضاً:أحداث أخرى في 1953تاريخ السعودية تحتوي هذه المقالة على أهم الأحداث التي شهدتها السعودية في 1953، إضافة إلى أهم الشخصيات السعودية التي وُلدت أو تُوفيت في هذه السنة. السياسة الحكم الملك: عبد العزيز بن عبد الرحمن آل سعود، حتى 9 ن...

 

 

Sherlock (EP)

2012 EP by ShineeSherlockEP by ShineeReleasedMarch 19, 2012 (2012-03-19)GenreK-popLength25:37LanguageKoreanLabelSM EntertainmentProducer Thomas Troelsen Pegasus Thomas Eriksen Niara Scarlett Philippe-Marc Anquetil Christopher Lee-Joe Iain James Yoo Han-jin Kenzie Brandon Fraley Shinee chronology The First(2011) Sherlock(2012) Boys Meet U(2013) Singles from Sherlock Sherlock (Clue + Note)Released: March 19, 2012 Music videoSherlock (Clue + Note) on YouTube Sherlock is t...

 

 

Eisteddfod

Véase también: Eisteddfod Nacional de GalesEisteddfod de 1991 Eisteddfod de 1958 El Eisteddfod es una festividad de origen galés, que comenzó a celebrarse en el siglo XII, cuando el conde Rhys ap Gruffyddd de Deheubarth organizó esta festividad y competición de poesía y música, en Cardigan en 1176. Los poetas galeses se reunían cada año para relatar sus poesías y escritos, y así competir entre ellos para obtener un lugar en la mesa del príncipe que organizaba el certamen, ga...

The Night Watch

1642 painting by Rembrandt This article is about the Rembrandt painting. For other uses, see Night Watch. You can help expand this article with text translated from the corresponding article in Dutch. (January 2023) Click [show] for important translation instructions. Machine translation, like DeepL or Google Translate, is a useful starting point for translations, but translators must revise errors as necessary and confirm that the translation is accurate, rather than simply copy-pasting...

 

 

Murasaki Shikibu

Japanese novelist and poet (c. 973 – c. 1014) Lady Murasaki redirects here. For the character, see Murasaki no Ue. Depiction of Murasaki Shikibu by Tosa Mitsuoki Murasaki Shikibu (紫式部, 'Lady Murasaki'; c. 973 – c. 1014 or 1025) was a Japanese novelist, poet and lady-in-waiting at the Imperial court in the Heian period. She is best known as the author of The Tale of Genji, widely considered to be one of the world's first novels, written in Japanese between about 1000...