matita.cs.unibo.it Git - helm.git/blob - helm/www/matita/matita.shtml

1

2

3 <html xmlns="http://www.w3.org/1999/xhtml">

4 <head>

5 <meta name="keywords" content="Matita, prover, assistant" />

6 <title>Matita - Home Page</title>

7

8 </head>

9 <body>

10

11

12 <div class="main">

13

14 <div class="topimage">

15 <img src="images/matita-text-big.png" alt="Matita" />

16 <a href="matita_it.shtml">

17 <img src="flags/wit.gif" alt="italian flag" />

18 </a>

19 </div>

20

21

22 Matita (that means pencil in italian) is an experimental,

23 interactive theorem prover under development at the

24 <a href="http://www.cs.unibo.it">Computer Science Department</a> of the

25 <a href="http://www.unibo.it">University of Bologna</a>.

26

27

28

29

30

31

32 <a class="quiet" href="images/screenshot-matita.png">

33 <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />

34 </a>

35

36

37 Matita is based on the

38 Calculus of (Co)Inductive Constructions, and is compatible, at some

39 extent, with <a href="http://coq.inria.fr">Coq</a>.

40 It is a reasonably small and simple application, whose

41 architectural and software complexity is meant to be mastered by

42 students, providing a tool particularly suited for testing innovative

43 ideas and solutions.

44 Matita adopts a tactic based editing mode; (XML-encoded) proof objects

45 are produced for storage and exchange.

46

47

48

49

50 <a class="quiet" href="images/screenshot-matita-href.png">

51 <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />

52 </a>

53 <a class="quiet" href="images/screenshot-matita-selection.png">

54 <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />

55 </a>

56

57 The graphical interface has been inspired by CtCoq and

58 <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.

59 It supports high quality bidimensional rendering of

60 proofs and formulae transformed on-the-fly to

61 <a href="http://www.w3.org/Math/">MathML</a> markup

62

63

64

65 <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">

66 <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />

67 </a>

68 <a class="quiet" href="images/screenshot-cicbrowser-query.png">

69 <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />

70 </a>

71 <!--

72 <a class="quiet" href="images/screenshot-cicbrowser-proof.png">

73 <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"

74 </a>

75 -->

76

77

78 The <a href="library.shtml">knowledge base</a> can be

79 <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>

80 (locally or on the World Wide Web) and

81 <a href="http://helm.cs.unibo.it/whelp/"> searched by means of

82 content-based queries</a>;

83

84

85

86 <a class="quiet" href="images/screenshot-tinycals.png">

87 <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />

88 </a>

89

90 The tactical language, part of the proof language, has

91 step-by-step semantics, enabling inspection and replaying of deeply

92 structured proof scripts.

93

94 Matita is partially supported by the following Projects:

95 <ul>

96 <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">

97 Types Project</a></li>

98 <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>

99 <li><a href="http://dama.cs.unibo.it/">Dama</a></li>

100 </ul>

101

102

103 </div>

104 </body>

105 </html>