helm/software/matita/help/C/matita.xml

   1 <?xml version="1.0"?>
   2 <!DOCTYPE article PUBLIC "-//OASIS//DTD DocBook XML V4.1.2//EN"
   3     "http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [
   4   <!ENTITY legal SYSTEM "legal.xml">
   5   <!ENTITY appversion "0.0">
   6   <!ENTITY manrevision "0.0">
   7   <!ENTITY date "February 2006">
   8   <!ENTITY app "<application>Matita</application>">
   9   <!ENTITY appname "Matita">
  10   <!ENTITY version "0.0">
  11 ]>
  12
  13 <!-- =============Document Header ============================= -->
  14 <article id="index" lang="en">
  15 <!-- please do not change the id; for translations, change lang to -->
  16 <!-- appropriate code -->
  17 <articleinfo>
  18  <title>&app; Manual V&manrevision;</title>
  19
  20  <copyright>
  21   <year>2006</year>
  22   <holder>The HELM team.</holder>
  23  </copyright>
  24 <!-- translators: uncomment this:
  25
  26   <copyright>
  27    <year>2002</year>
  28    <holder>ME-THE-TRANSLATOR (Latin translation)</holder>
  29   </copyright>
  30
  31    -->
  32 <!-- An address can be added to the publisher information.  If a role is
  33      not specified, the publisher/author is the same for all versions of the
  34      document.  -->
  35 <!-- CSC:
  36     <publisher>
  37       <publishername> GNOME Documentation Project </publishername>
  38     </publisher>
  39 -->
  40
  41    &legal;
  42    <!-- This file  contains link to license for the documentation (GNU FDL), and
  43         other legal stuff such as "NO WARRANTY" statement. Please do not change
  44         any of this. -->
  45
  46     <authorgroup>
  47       <author>
  48         <firstname>Andrea</firstname>
  49         <surname>Asperti</surname>
  50         <affiliation>
  51           <address> <email>asperti@cs.unibo.it</email> </address>
  52         </affiliation>
  53       </author>
  54       <author>
  55         <firstname>Claudio</firstname>
  56         <surname>Sacerdoti Coen</surname>
  57         <affiliation>
  58           <address> <email>sacerdot@cs.unibo.it</email> </address>
  59         </affiliation>
  60       </author>
  61       <author>
  62         <firstname>Enrico</firstname>
  63         <surname>Tassi</surname>
  64         <affiliation>
  65           <address> <email>tassi@cs.unibo.it</email> </address>
  66         </affiliation>
  67       </author>
  68       <author>
  69         <firstname>Stefano</firstname>
  70         <surname>Zacchiroli</surname>
  71         <affiliation>
  72           <address> <email>zacchiro@cs.unibo.it</email> </address>
  73         </affiliation>
  74       </author>
  75 <!-- This is appropriate place for other contributors: translators,
  76       maintainers,  etc. Commented out by default.
  77        <othercredit role="translator">
  78         <firstname>Latin</firstname>
  79         <surname>Translator 1</surname>
  80         <affiliation>
  81           <orgname>Latin Translation Team</orgname>
  82           <address> <email>translator@gnome.org</email> </address>
  83         </affiliation>
  84         <contrib>Latin translation</contrib>
  85       </othercredit>
  86 -->
  87     </authorgroup>
  88
  89 <revhistory>
  90       <revision>
  91         <revnumber>&appname; Manual V&manrevision;</revnumber>
  92         <date>&date;</date>
  93         <revdescription>
  94           <para role="author">The HELM team
  95 <!--
  96             <email>baudais@okstate.edu</email>
  97 -->
  98           </para>
  99 <!--
 100           <para role="publisher">GNOME Documentation Project</para>
 101 -->
 102         </revdescription>
 103       </revision>
 104   <revision>
 105    <revnumber>0.0</revnumber>
 106    <date>4 February 2006</date>
 107    <authorinitials>HELM</authorinitials>
 108    <revremark>
 109    First draft completed.
 110    </revremark>
 111   </revision>
 112
 113  </revhistory>
 114
 115     <releaseinfo>This manual describes version &appversion; of &appname;.
 116     </releaseinfo>
 117     <!-- The following feedback information only applies to appliactions
 118     listed in bugzilla.gnome.org and bugzilla.ximian.com. For other
 119     applications, please provide your own feedback info or remove thsi
 120     section altogether -->
 121     <legalnotice>
 122       <title>Feedback</title>
 123       <para>To report a bug or make a suggestion regarding the &app; application or
 124         this manual, follow the directions in the
 125         <ulink url="http://mowgli.cs.unibo.it/bugs"
 126           type="help">HELM Bugzilla Page</ulink>.
 127       </para>
 128 <!-- Translators may also add here feedback address for translations -->
 129     </legalnotice>
 130
 131 </articleinfo>
 132
 133   <indexterm zone="index">
 134     <primary>Matita</primary>
 135   </indexterm>
 136
 137 <!-- ============= Document Body ============================= -->
 138 <!-- ============= Introduction ============================== -->
 139 <sect1 id="intro">
 140  <title>Introduction</title>
 141  <sect2 id="what">
 142   <title>What is Matita?</title>
 143
 144   <para>
 145   <application>Matita</application> is a proof assistant for ...
 146   </para>
 147
 148  </sect2>
 149 </sect1>
 150
 151 <!-- =========== Terms, declarations and definitions ============ -->
 152 <sect1 id="terms_decl_def">
 153  <title>Terms, definitions, declarations and proofs</title>
 154  <sect2 id="terms">
 155  <title>Terms</title>
 156  </sect2>
 157  <sect2 id="definitions">
 158  <title>Definitions</title>
 159  </sect2>
 160  <sect2 id="declarations">
 161  <title>Declarations (of inductive types)</title>
 162  </sect2>
 163  <sect2 id="proofs">
 164  <title>Proofs</title>
 165  </sect2>
 166 </sect1>
 167
 168 <!-- ============ Tactics ====================== -->
 169 <sect1 id="tactics">
 170  <title>Tactics</title>
 171
 172   <sect2 id="tac_absurd">
 173     <title>absurd &lt;term&gt;</title>
 174     <para>The tactic <command>absurd</command> </para>
 175 <para>
 176 <ulink url="#terms">ciao</ulink>
 177 </para>
 178   </sect2>
 179   <sect2 id="tac_apply">
 180     <title>apply &lt;term&gt;</title>
 181     <para>The tactic <command>apply</command> </para>
 182   </sect2>
 183   <sect2 id="tac_assumption">
 184     <title>assumption</title>
 185     <para>The tactic <command>assumption</command> </para>
 186   </sect2>
 187   <sect2 id="tac_auto">
 188     <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
 189     <para>The tactic <command>auto</command> </para>
 190   </sect2>
 191   <sect2 id="tac_clear">
 192     <title>clear &lt;id&gt;</title>
 193     <para>The tactic <command>clear</command> </para>
 194   </sect2>
 195   <sect2 id="tac_clearbody">
 196     <title>clearbody &lt;id&gt;</title>
 197     <para>The tactic <command>clearbody</command> </para>
 198   </sect2>
 199   <sect2 id="tac_change">
 200     <title>change &lt;pattern&gt; with &lt;term&gt;</title>
 201     <para>The tactic <command>change</command> </para>
 202   </sect2>
 203   <sect2 id="tac_compare">
 204     <title>compare &lt;term&gt;</title>
 205     <para>The tactic <command>compare</command> </para>
 206   </sect2>
 207   <sect2 id="tac_constructor">
 208     <title>constructor &lt;int&gt;</title>
 209     <para>The tactic <command>constructor</command> </para>
 210   </sect2>
 211   <sect2 id="tac_contradiction">
 212     <title>contradiction</title>
 213     <para>The tactic <command>contradiction</command> </para>
 214   </sect2>
 215   <sect2 id="tac_cut">
 216     <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
 217     <para>The tactic <command>cut</command> </para>
 218   </sect2>
 219   <sect2 id="tac_decide equality">
 220     <title>decide</title>
 221     <para>The tactic <command>decide equality</command> </para>
 222   </sect2>
 223   <sect2 id="tac_decompose">
 224     <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
 225     <para>The tactic <command>decompose</command> </para>
 226   </sect2>
 227   <sect2 id="tac_discriminate">
 228     <title>discriminate &lt;term&gt;</title>
 229     <para>The tactic <command>discriminate</command> </para>
 230   </sect2>
 231   <sect2 id="tac_elim">
 232     <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
 233     <para>The tactic <command>elim</command> </para>
 234   </sect2>
 235   <sect2 id="tac_elimType">
 236     <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
 237     <para>The tactic <command>elimType</command> </para>
 238   </sect2>
 239   <sect2 id="tac_exact">
 240     <title>exact &lt;term&gt;</title>
 241     <para>The tactic <command>exact</command> </para>
 242   </sect2>
 243   <sect2 id="tac_exists">
 244     <title>exists</title>
 245     <para>The tactic <command>exists</command> </para>
 246   </sect2>
 247   <sect2 id="tac_fail">
 248     <title>fail</title>
 249     <para>The tactic <command>fail</command> </para>
 250   </sect2>
 251   <sect2 id="tac_fold">
 252     <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
 253     <para>The tactic <command>fold</command> </para>
 254   </sect2>
 255   <sect2 id="tac_fourier">
 256     <title>fourier</title>
 257     <para>The tactic <command>fourier</command> </para>
 258   </sect2>
 259   <sect2 id="tac_fwd">
 260     <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
 261     <para>The tactic <command>fwd</command> </para>
 262   </sect2>
 263   <sect2 id="tac_generalize">
 264     <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
 265     <para>The tactic <command>generalize</command> </para>
 266   </sect2>
 267   <sect2 id="tac_id">
 268     <title>id</title>
 269     <para>The tactic <command>id</command> </para>
 270   </sect2>
 271   <sect2 id="tac_injection">
 272     <title>injection &lt;term&gt;</title>
 273     <para>The tactic <command>injection</command> </para>
 274   </sect2>
 275   <sect2 id="tac_intro">
 276     <title>intro [&lt;ident&gt;]</title>
 277     <para>The tactic <command>intro</command> </para>
 278   </sect2>
 279   <sect2 id="tac_intros">
 280     <title>intros &lt;intros_spec&gt;</title>
 281     <para>The tactic <command>intros</command> </para>
 282   </sect2>
 283   <sect2 id="tac_inversion">
 284     <title>intros &lt;term&gt;</title>
 285     <para>The tactic <command>intros</command> </para>
 286   </sect2>
 287   <sect2 id="tac_lapply">
 288     <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
 289     <para>The tactic <command>lapply</command> </para>
 290   </sect2>
 291   <sect2 id="tac_left">
 292     <title>left</title>
 293     <para>The tactic <command>left</command> </para>
 294   </sect2>
 295   <sect2 id="tac_letin">
 296     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
 297     <para>The tactic <command>letin</command> </para>
 298   </sect2>
 299   <sect2 id="tac_normalize">
 300     <title>normalize &lt;pattern&gt;</title>
 301     <para>The tactic <command>normalize</command> </para>
 302   </sect2>
 303   <sect2 id="tac_paramodulation">
 304     <title>paramodulation &lt;pattern&gt;</title>
 305     <para>The tactic <command>paramodulation</command> </para>
 306   </sect2>
 307   <sect2 id="tac_reduce">
 308     <title>reduce &lt;pattern&gt;</title>
 309     <para>The tactic <command>reduce</command> </para>
 310   </sect2>
 311   <sect2 id="tac_reflexivity">
 312     <title>reflexivity</title>
 313     <para>The tactic <command>reflexivity</command> </para>
 314   </sect2>
 315   <sect2 id="tac_replace">
 316     <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
 317     <para>The tactic <command>replace</command> </para>
 318   </sect2>
 319   <sect2 id="tac_rewrite">
 320     <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
 321     <para>The tactic <command>rewrite</command> </para>
 322   </sect2>
 323   <sect2 id="tac_right">
 324     <title>right</title>
 325     <para>The tactic <command>right</command> </para>
 326   </sect2>
 327   <sect2 id="tac_ring">
 328     <title>ring</title>
 329     <para>The tactic <command>ring</command> </para>
 330   </sect2>
 331   <sect2 id="tac_simplify">
 332     <title>simplify &lt;pattern&gt;</title>
 333     <para>The tactic <command>simplify</command> </para>
 334   </sect2>
 335   <sect2 id="tac_split">
 336     <title>split</title>
 337     <para>The tactic <command>split</command> </para>
 338   </sect2>
 339   <sect2 id="tac_symmetry">
 340     <title>symmetry</title>
 341     <para>The tactic <command>symmetry</command> </para>
 342   </sect2>
 343   <sect2 id="tac_transitivity">
 344     <title>transitivity &lt;term&gt;</title>
 345     <para>The tactic <command>transitivity</command> </para>
 346   </sect2>
 347   <sect2 id="tac_unfold">
 348     <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
 349     <para>The tactic <command>unfold</command> </para>
 350   </sect2>
 351   <sect2 id="tac_whd">
 352     <title>whd &lt;pattern&gt;</title>
 353     <para>The tactic <command>whd</command> </para>
 354   </sect2>
 355
 356 </sect1>
 357
 358  <!-- ============= Application License ============================= -->
 359
 360  <sect1 id="license">
 361   <title>License</title>
 362   <para>
 363    This program is free software; you can redistribute it and/or
 364    modify it under the terms of the <citetitle>GNU General Public
 365    License</citetitle> as published by the Free Software Foundation;
 366    either version 2 of the License, or (at your option) any later
 367    version.
 368   </para>
 369   <para>
 370    This program is distributed in the hope that it will be useful, but
 371    WITHOUT ANY WARRANTY; without even the implied warranty of
 372    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 373    <citetitle>GNU General Public License</citetitle> for more details.
 374   </para>
 375   <para>
 376    A copy of the <citetitle>GNU General Public License</citetitle> is
 377    included as an appendix to the <citetitle>GNOME Users
 378    Guide</citetitle>.  You may also obtain a copy of the
 379    <citetitle>GNU General Public License</citetitle> from the Free
 380    Software Foundation by visiting <ulink type="http"
 381    url="http://www.fsf.org">their Web site</ulink> or by writing to
 382    <address>
 383     Free Software Foundation, Inc.
 384     <street>59 Temple Place</street> - Suite 330
 385     <city>Boston</city>, <state>MA</state> <postcode>02111-1307</postcode>
 386     <country>USA</country>
 387    </address>
 388   </para>
 389  </sect1>
 390 </article>
 391
 392 <!-- CSC: valid element tags
 393 <sect1 id="intro"> <title>Introduction</title> ...
 394 <sect2 id="what"> <title>What is Matita?</title>
 395 <para>
 396 <note> <title>Note:</title> <para> ...
 397 <footnote> <para> ...
 398 <itemizedlist mark="opencircle">
 399     <listitem>
 400      <para>
 401         The computer player for Iagno is easy to beat.
 402      </para>
 403     </listitem>
 404  </itemizedlist>
 405
 406 <ulink type="http" url="http://www.gnome.org/gdp">
 407 <email>itp@gnu.org</email>
 408 <application>Matita</application>
 409 <command>iagno</command> on the command line
 410 <citetitle>Othello</citetitle>
 411
 412 <guimenuitem>Iagno</guimenuitem>
 413 <guisubmenu>Games</guisubmenu>
 414 <guibutton>none</guibutton>
 415 <menuchoice> <guimenu>Settings</guimenu> <guisubmenu>Preferences </guisubmenu> </menuchoice>
 416
 417 <xref linkend="start-shot"/>.
 418 <figure id="start-shot">
 419  <title>Starting Position</title>
 420  <screenshot>
 421    <mediaobject>
 422    <imageobject>
 423  <imagedata fileref="figures/START.png" format="PNG" srccredit="Eric Baudais"/>
 424   </imageobject>
 425    <textobject>
 426      <phrase>Screenshot of the starting position.</phrase>
 427    </textobject>
 428  </mediaobject>
 429  </screenshot>
 430 </figure>
 431
 432 -->