Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 4

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

Tarski Geometry Axioms

100%
Richter W., Grabowski A., Alama J.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
167-176
EN
This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work. The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms. This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line. The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski’s geometry related to real planes were constructed.
2
Content available remote

Tarski Geometry Axioms – Part II

100%
Coghetto R., Grabowski A.
Formalized Mathematics
|
2016
|
tom 24
|
nr 2
157-166
EN
In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates: of betweenness between (a ternary relation), of congruence of segments equiv (quarternary relation), which satisfy the following properties: congruence symmetry (A1), congruence equivalence relation (A2), congruence identity (A3), segment construction (A4), SAS (A5), betweenness identity (A6), Pasch (A7). Also a simple model, which satisfies these axioms, was previously constructed, and described in [6]. In this paper, we deal with four remaining axioms, namely: the lower dimension axiom (A8), the upper dimension axiom (A9), the Euclid axiom (A10), the continuity axiom (A11). They were introduced in the form of Mizar attributes. Additionally, the relation of congruence of triangles cong is introduced via congruence of sides (SSS). In order to show that the structure which satisfies all eleven Tarski’s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural [5] extension of ordinary metric structure Euclid 2 satisfies all these attributes. Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq [11], first approaches to this topic were done in Mizar in 1990 [16] (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time [8]). Connection with another proof assistant should be mentioned – we had some doubts about the proof of the Euclid’s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle [10] clarified things a bit. Our development allows for the future faithful mechanization of [13] and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory [7].
3
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

Several observations about Maneeals - a peculiar system of lines

100%
Dasari N. V. K., Kabat J.
Annales Universitatis Paedagogicae Cracoviensis. Studia Mathematica
|
2016
|
tom 15
EN
For an arbitrary triangle ABC and an integer n we define points Dn, En, Fn on the sides BC, CA, AB respectively, in such a manner that |AC|n|AB|n=|CDn||BDn|,|AB|n|BC|n=|AEn||CEn|,|BC|n|AC|n=|BFn||AFn|. $$\matrix{{{{\left| {AC} \right|^n } \over {\left| {AB} \right|^n }} = {{\left| {CD_n } \right|} \over {\left| {BD_n } \right|}},} \hfill & {{{\left| {AB} \right|^n } \over {\left| {BC} \right|^n }} = {{\left| {AE_n } \right|} \over {\left| {CE_n } \right|}},} \hfill & {{{\left| {BC} \right|^n } \over {\left| {AC} \right|^n }} = {{\left| {BF_n } \right|} \over {\left| {AF_n } \right|}}.}} $$ Cevians ADn, BEn, CFn are said to be the Maneeals of order n. In this paper we discuss some properties of the Maneeals and related objects.
4
Content available remote

Does any convex quadrilateral have circumscribed ellipses?

84%
Li J. H., Wang Z. Q., Shen Y. X., Dai Z. Y.
Open Mathematics
|
2017
|
tom 15
|
nr 1
1463-1476
EN
The past decades have witnessed several well-known beautiful conclusions on four con-cyclic points. With highly promising research value, we profoundly studied circumscribed ellipses of convex quadrilaterals in this paper. Using tools of parallel projective transformation and analytic geometry, we derived several theorems including the proof of the existence of circumscribed ellipses of convex quadrilaterals, the properties of its minimal coverage area, and locus center, respectively. This simple approach lays a solid foundation for its application to three-dimensional situations, which is namely the circumscribed quadric surface of a solid figure and its wide-range utility in construction engineering. Meanwhile, we have a new insight into innate connection of conic sections as well as a taste of beauty and harmony of geometry.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.