1. Research with MATF
  2. MATF
  3. Research outputs
Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/601
DC FieldValueLanguage
dc.contributor.authorSimić, Danijelaen_US
dc.contributor.authorMarić, Filipen_US
dc.contributor.authorBoutry, Pierreen_US
dc.date.accessioned2022-08-13T15:50:05Z-
dc.date.available2022-08-13T15:50:05Z-
dc.date.issued2021-01-01-
dc.identifier.issn01687433en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/601-
dc.description.abstractWe describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line CP1and is shown to satisfy Tarski’s axioms except for Euclid’s axiom—it is shown to satisfy it’s negation, and, moreover, to satisfy the existence of limiting parallels axiom.en
dc.relation.ispartofJournal of Automated Reasoningen
dc.subjectFormalization of geometryen
dc.subjectIsabelle/HOLen
dc.subjectPoincaré modelen
dc.titleFormalization of the Poincaré Disc Model of Hyperbolic Geometryen_US
dc.typeArticleen_US
dc.identifier.doi10.1007/s10817-020-09551-2-
dc.identifier.scopus2-s2.0-85084221149-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/85084221149-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage31en
dc.relation.lastpage73en
dc.relation.volume65en
dc.relation.issue1en
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeArticle-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0002-3840-9931-
crisitem.author.orcid0000-0001-7219-6960-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

3
checked on Dec 22, 2024

Page view(s)

14
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.