From: Ferruccio Guidi Date: Thu, 28 Nov 2013 16:07:56 +0000 (+0000) Subject: update in ground_2, web page for ground_2 X-Git-Tag: make_still_working~1041 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c9a1672c725945b47f9ea8af3c23b67cf9026f01;p=helm.git update in ground_2, web page for ground_2 --- diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html new file mode 100644 index 000000000..05e7beabe --- /dev/null +++ b/helm/www/lambdadelta/ground_2.html @@ -0,0 +1,199 @@ + + + + + + + + + + lambdadelta version 2 + + + + + + +
+ + [lambdadelta home] + +
+
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
+
+ [Spacer] +
+
Summary of the Specification
+
Here is a numerical acount of the specification's contents + and its timeline. + Nodes are counted according to the "intrinsinc complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), + pp. 53-78]. +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects +
+ 		+
+ 		+
+ 		+
+ 		+
+
sizesfiles24 characters62302nodes38860
propositionstheorems2lemmas88total90
conceptsdeclared40defined22total62
+
+ + + +
Logical Structure of the Specification
+
The source files are grouped in planes + according to the following table. + Notation files covering the whole specification are provided. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
planefiles +
+ 		+
+ 		+
+ 		+
+
natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )
extensions to the libraryarith.ma ( ?^? ) +
+ 		+
+ 		+
+ 		+
+
generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
+ 		+
+ 		+
+
+
+ +
Physical Structure of the Specification
+
The source files are grouped in directories, + one for each plane. +
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Thu, 28 Nov 2013 17:05:53 +0100
+ + diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 915d3193d..55d01c4dd 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -71,6 +71,8 @@ specification of λδ version 2 and related topics is restarted in Here is a page about the specification (Core). +
  • Here is a page about the +background of the specification (Ground).
    • @@ -225,7 +227,7 @@ this site as the first result. Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"> [Use Any Browser Here] [PNG Used Here]

    -Last update 2012-12-02 by Ferruccio +Last update 2013-10-27 by Ferruccio Guidi