Commit 1e77aee3 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

paragraph tags in the abstract of IsaGeoCoq

parent d7023101f4f1
......@@ -2031,30 +2031,30 @@ license = LGPL
date = 2021-01-31
notify = roland_coghetto@hotmail.com
abstract =
The <a href="https://geocoq.github.io/GeoCoq/">GeoCoq library</a> contains a formalization
of geometry using the Coq proof assistant. It contains both proofs
about the foundations of geometry and high-level proofs in the same
style as in high school. We port a part of the GeoCoq
2.4.0 library to Isabelle/HOL: more precisely,
the files Chap02.v to Chap13_3.v, suma.v as well as the associated
definitions and some useful files for the demonstration of certain
parallel postulates. The synthetic approach of the demonstrations is directly
inspired by those contained in GeoCoq. The names of the lemmas and
theorems used are kept as far as possible as well as the definitions.
It should be noted that T.J.M. Makarios has done
<a href="https://www.isa-afp.org/entries/Tarskis_Geometry.html">some proofs in Tarski's Geometry</a>. It uses a definition that does not quite
coincide with the definition used in Geocoq and here.
Furthermore, corresponding definitions in the <a href="https://www.isa-afp.org/entries/Poincare_Disc.html">Poincaré Disc Model
development</a>
are not not identical to those defined in GeoCoq.
In the last part, it is
formalized that, in the neutral/absolute space, the axiom of the
parallels of Tarski's system implies the Playfair axiom, the 5th
postulate of Euclid and Euclid's original parallel postulate. These
proofs, which are not constructive, are directly inspired by Pierre
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.
<p>The <a href="https://geocoq.github.io/GeoCoq/">GeoCoq library</a> contains a formalization
of geometry using the Coq proof assistant. It contains both proofs
about the foundations of geometry and high-level proofs in the same
style as in high school. We port a part of the GeoCoq
2.4.0 library to Isabelle/HOL: more precisely,
the files Chap02.v to Chap13_3.v, suma.v as well as the associated
definitions and some useful files for the demonstration of certain
parallel postulates. The synthetic approach of the demonstrations is directly
inspired by those contained in GeoCoq. The names of the lemmas and
theorems used are kept as far as possible as well as the definitions.
</p>
<p>It should be noted that T.J.M. Makarios has done
<a href="https://www.isa-afp.org/entries/Tarskis_Geometry.html">some proofs in Tarski's Geometry</a>. It uses a definition that does not quite
coincide with the definition used in Geocoq and here.
Furthermore, corresponding definitions in the <a href="https://www.isa-afp.org/entries/Poincare_Disc.html">Poincaré Disc Model
development</a> are not identical to those defined in GeoCoq.
</p>
<p>In the last part, it is
formalized that, in the neutral/absolute space, the axiom of the
parallels of Tarski's system implies the Playfair axiom, the 5th
postulate of Euclid and Euclid's original parallel postulate. These
proofs, which are not constructive, are directly inspired by Pierre
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.
</p>
 
[General-Triangle]
title = The General Triangle Is Unique
......
......@@ -143,7 +143,7 @@ MathJax = {
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
The <a href="https://geocoq.github.io/GeoCoq/">GeoCoq library</a> contains a formalization
<p>The <a href="https://geocoq.github.io/GeoCoq/">GeoCoq library</a> contains a formalization
of geometry using the Coq proof assistant. It contains both proofs
about the foundations of geometry and high-level proofs in the same
style as in high school. We port a part of the GeoCoq
......@@ -153,18 +153,20 @@ definitions and some useful files for the demonstration of certain
parallel postulates. The synthetic approach of the demonstrations is directly
inspired by those contained in GeoCoq. The names of the lemmas and
theorems used are kept as far as possible as well as the definitions.
It should be noted that T.J.M. Makarios has done
</p>
<p>It should be noted that T.J.M. Makarios has done
<a href="https://www.isa-afp.org/entries/Tarskis_Geometry.html">some proofs in Tarski's Geometry</a>. It uses a definition that does not quite
coincide with the definition used in Geocoq and here.
Furthermore, corresponding definitions in the <a href="https://www.isa-afp.org/entries/Poincare_Disc.html">Poincaré Disc Model
development</a>
are not not identical to those defined in GeoCoq.
In the last part, it is
development</a> are not identical to those defined in GeoCoq.
</p>
<p>In the last part, it is
formalized that, in the neutral/absolute space, the axiom of the
parallels of Tarski's system implies the Playfair axiom, the 5th
postulate of Euclid and Euclid's original parallel postulate. These
proofs, which are not constructive, are directly inspired by Pierre
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.</td>
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.
</p></td>
</tr>
......
......@@ -17,7 +17,7 @@
<dc:creator> Roland Coghetto </dc:creator>
<pubDate>31 Jan 2021 00:00:00 +0000</pubDate>
<description>
The &lt;a href=&#34;https://geocoq.github.io/GeoCoq/&#34;&gt;GeoCoq library&lt;/a&gt; contains a formalization
&lt;p&gt;The &lt;a href=&#34;https://geocoq.github.io/GeoCoq/&#34;&gt;GeoCoq library&lt;/a&gt; contains a formalization
of geometry using the Coq proof assistant. It contains both proofs
about the foundations of geometry and high-level proofs in the same
style as in high school. We port a part of the GeoCoq
......@@ -27,18 +27,20 @@ definitions and some useful files for the demonstration of certain
parallel postulates. The synthetic approach of the demonstrations is directly
inspired by those contained in GeoCoq. The names of the lemmas and
theorems used are kept as far as possible as well as the definitions.
It should be noted that T.J.M. Makarios has done
&lt;/p&gt;
&lt;p&gt;It should be noted that T.J.M. Makarios has done
&lt;a href=&#34;https://www.isa-afp.org/entries/Tarskis_Geometry.html&#34;&gt;some proofs in Tarski&#39;s Geometry&lt;/a&gt;. It uses a definition that does not quite
coincide with the definition used in Geocoq and here.
Furthermore, corresponding definitions in the &lt;a href=&#34;https://www.isa-afp.org/entries/Poincare_Disc.html&#34;&gt;Poincaré Disc Model
development&lt;/a&gt;
are not not identical to those defined in GeoCoq.
In the last part, it is
development&lt;/a&gt; are not identical to those defined in GeoCoq.
&lt;/p&gt;
&lt;p&gt;In the last part, it is
formalized that, in the neutral/absolute space, the axiom of the
parallels of Tarski&#39;s system implies the Playfair axiom, the 5th
postulate of Euclid and Euclid&#39;s original parallel postulate. These
proofs, which are not constructive, are directly inspired by Pierre
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.</description>
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.
&lt;/p&gt;</description>
</item>
<item>
<title>JinjaDCI: a Java semantics with dynamic class initialization</title>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment