helm/www/lambdadelta/ground_2.html

   1 <?xml version="1.0" encoding="UTF-8"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
   3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
   4   <head>
   5     <meta http-equiv="Content-Language" content="en-us" />
   6     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
   7     <meta http-equiv="Content-Style-Type" content="text/css" />
   8     <meta name="author" content="Ferruccio Guidi" />
   9     <meta name="description" content="background for \lambda\delta version 2" />
  10     <title>background for \lambda\delta version 2</title>
  11     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
  12     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
  13     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
  14     <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
  15   </head>
  16   <body lang="en-US">
  17     <div class="spacer">
  18       <a href="http://lambdadelta.info/">
  19         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
  20       </a>
  21     </div>
  22     <div class="head1">cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)</div>
  23     <div class="spacer">
  24       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
  25     </div>
  26    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Summary of the Specification</div>
  27    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
  28          and its timeline.
  29          Nodes are counted according to the "intrinsinc complexity measure"
  30          [F. Guidi: "Procedural Representation of CIC Proof Terms"
  31          Journal of Automated Reasoning 44(1-2), Springer (February 2010),
  32          pp. 53-78].
  33    </div>
  34    <div xmlns:ld="http://lambdadelta.info/" class="text">
  35       <table cellpadding="4" cellspacing="0">
  36         <tbody>
  37           <tr>
  38             <td class="snns capitalize italic gray">category</td>
  39             <td class="snns italic gray">objects</td>
  40             <td class="snnn right italic gray">
  41               <br />
  42             </td>
  43             <td class="snnn italic gray">
  44               <br />
  45             </td>
  46             <td class="snnn right italic gray">
  47               <br />
  48             </td>
  49             <td class="snnn italic gray">
  50               <br />
  51             </td>
  52             <td class="ssnn right italic gray">
  53               <br />
  54             </td>
  55           </tr>
  56           <tr>
  57             <td class="snns capitalize italic cyan">sizes</td>
  58             <td class="snns italic cyan">files</td>
  59             <td class="snnn right italic cyan">30</td>
  60             <td class="snns italic cyan">characters</td>
  61             <td class="snnn right italic cyan">68581</td>
  62             <td class="snns italic cyan">nodes</td>
  63             <td class="ssnn right italic cyan">62380</td>
  64           </tr>
  65           <tr>
  66             <td class="snns capitalize italic green">propositions</td>
  67             <td class="snns italic green">theorems</td>
  68             <td class="snnn right italic green">2</td>
  69             <td class="snns italic green">lemmas</td>
  70             <td class="snnn right italic green">187</td>
  71             <td class="snns italic green">total</td>
  72             <td class="ssnn right italic green">189</td>
  73           </tr>
  74           <tr>
  75             <td class="snss capitalize italic yellow">concepts</td>
  76             <td class="snss italic yellow">declared</td>
  77             <td class="snsn right italic yellow">40</td>
  78             <td class="snss italic yellow">defined</td>
  79             <td class="snsn right italic yellow">25</td>
  80             <td class="snss italic yellow">total</td>
  81             <td class="sssn right italic yellow">65</td>
  82           </tr>
  83         </tbody>
  84       </table>
  85     </div>
  86    <ul xmlns:ld="http://lambdadelta.info/">
  87       <li>
  88         <span class="date">2013 November 27.</span>
  89          Natural numbers with infinity.
  90    </li>
  91     </ul>
  92    <ul xmlns:ld="http://lambdadelta.info/">
  93       <li>
  94         <span class="date">2011 August 10.</span>
  95          Specification starts.
  96    </li>
  97     </ul>
  98
  99    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Logical Structure of the Specification</div>
 100    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes
 101          according to the following table.
 102          Notation files covering the whole specification are provided.
 103          The notation for the relations or functions introduced in each file
 104          is shown in parentheses (? are placeholders).
 105    </div>
 106    <div xmlns:ld="http://lambdadelta.info/" class="text">
 107       <table cellpadding="4" cellspacing="0">
 108         <tbody>
 109           <tr>
 110             <td class="snns top italic gray">plane</td>
 111             <td class="snns top gray">files</td>
 112             <td class="snnn top gray">
 113               <br />
 114             </td>
 115             <td class="snnn top gray">
 116               <br />
 117             </td>
 118             <td class="snnn top gray">
 119               <br />
 120             </td>
 121             <td class="snnn top gray">
 122               <br />
 123             </td>
 124             <td class="snnn top gray">
 125               <br />
 126             </td>
 127             <td class="snnn top gray">
 128               <br />
 129             </td>
 130             <td class="snnn top gray">
 131               <br />
 132             </td>
 133             <td class="ssnn top gray">
 134               <br />
 135             </td>
 136           </tr>
 137           <tr>
 138             <td class="snns top italic yellow">natural numbers with infinity</td>
 139             <td class="snns top yellow">ynat ( ∞ )</td>
 140             <td class="snnn top yellow">ynat_pred ( ⫰? )</td>
 141             <td class="snnn top yellow">ynat_succ ( ⫯? )</td>
 142             <td class="snnn top yellow">ynat_le ( ?≤? )</td>
 143             <td class="snnn top yellow">ynat_lt ( ?&lt;? )</td>
 144             <td class="snnn top yellow">ynat_minus ( ? - ? )</td>
 145             <td class="snnn top yellow">ynat_plus ( ? + ? )</td>
 146             <td class="snnn top yellow">ynat_max</td>
 147             <td class="ssnn top yellow">ynat_min</td>
 148           </tr>
 149           <tr>
 150             <td class="snns top italic orange">extensions to the library</td>
 151             <td class="snns top orange">arith.ma ( ?^? )</td>
 152             <td class="snnn top orange">
 153               <br />
 154             </td>
 155             <td class="snnn top orange">
 156               <br />
 157             </td>
 158             <td class="snnn top orange">
 159               <br />
 160             </td>
 161             <td class="snnn top orange">
 162               <br />
 163             </td>
 164             <td class="snnn top orange">
 165               <br />
 166             </td>
 167             <td class="snnn top orange">
 168               <br />
 169             </td>
 170             <td class="snnn top orange">
 171               <br />
 172             </td>
 173             <td class="ssnn top orange">
 174               <br />
 175             </td>
 176           </tr>
 177           <tr>
 178             <td class="snss top italic red">generated logical decomposables</td>
 179             <td class="snss top red">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
 180             <td class="snsn top red">xoa_props ( ⊥ ) ( ⊤ )</td>
 181             <td class="snsn top red">
 182               <br />
 183             </td>
 184             <td class="snsn top red">
 185               <br />
 186             </td>
 187             <td class="snsn top red">
 188               <br />
 189             </td>
 190             <td class="snsn top red">
 191               <br />
 192             </td>
 193             <td class="snsn top red">
 194               <br />
 195             </td>
 196             <td class="snsn top red">
 197               <br />
 198             </td>
 199             <td class="sssn top red">
 200               <br />
 201             </td>
 202           </tr>
 203         </tbody>
 204       </table>
 205     </div>
 206
 207    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Physical Structure of the Specification</div>
 208    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
 209          one for each plane.
 210    </div>
 211    <div class="spacer">
 212       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 213     </div>
 214     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 215       <br />
 216     </div>
 217     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 218       <a href="http://validator.w3.org/check?uri=referer">
 219         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 220       </a>
 221       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 222         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 223       </a>
 224       <a href="http://www.w3.org/XML/">
 225         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 226       </a>
 227       <a href="http://www.w3.org/Graphics/PNG/">
 228         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 229       </a>
 230       <a href="http://www.anybrowser.org/campaign/">
 231         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 232       </a>
 233     </div>
 234     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 235       <br />
 236     </div>
 237     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 22 Oct 2014 20:00:29 +0200</div>
 238 </body>
 239 </html>