Matitais 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 Calculus of Constructions), and is compatible, to some extent, with Coq.
Property | Value |
---|---|
dbo:abstract |
|
dbo:developer | |
dbo:genre | |
dbo:license | |
dbo:operatingSystem | |
dbo:programmingLanguage | |
dbo:thumbnail | |
dbo:wikiPageExternalLink | |
dbo:wikiPageID |
|
dbo:wikiPageLength |
|
dbo:wikiPageRevisionID |
|
dbo:wikiPageWikiLink |
|
dbp:caption |
|
dbp:developer | |
dbp:genre | |
dbp:language |
|
dbp:license | |
dbp:logo |
|
dbp:name |
|
dbp:operatingSystem | |
dbp:programmingLanguage | |
dbp:released |
|
dbp:screenshot |
|
dbp:screenshotSize |
|
dbp:website | |
dbp:wikiPageUsesTemplate | |
dbp:wordnet_type | |
dcterms:subject | |
rdf:type |
|
rdfs:comment |
|
rdfs:label |
|
owl:sameAs | |
prov:wasDerivedFrom | |
foaf:depiction | |
foaf:homepage | |
foaf:isPrimaryTopicOf | |
foaf:name |
|
is dbo:wikiPageRedirects of | |
is dbo:wikiPageWikiLink of | |
is foaf:primaryTopic of |