Show simple item record

Formal systems for proving incidence results

dc.contributor.advisorPetrić, Zoran
dc.contributor.advisorBaralić, Đorđe
dc.contributor.otherGilezan, Silvia
dc.contributor.otherJaničić, Predrag
dc.contributor.otherDoroslovački, Ksenija
dc.contributor.otherPetrić, Zoran
dc.contributor.otherBaralić, Đorđe
dc.creatorMilićević, Marina
dc.date.accessioned2021-02-25T14:53:29Z
dc.date.available2021-02-25T14:53:29Z
dc.date.issued2020-10-28
dc.identifier.urihttps://www.cris.uns.ac.rs/DownloadFileServlet/Disertacija159480060455857.pdf?controlNumber=(BISIS)114829&fileName=159480060455857.pdf&id=16102&source=NaRDuS&language=srsr
dc.identifier.urihttps://www.cris.uns.ac.rs/record.jsf?recordId=114829&source=NaRDuS&language=srsr
dc.identifier.urihttps://www.cris.uns.ac.rs/DownloadFileServlet/IzvestajKomisije159480061237421.pdf?controlNumber=(BISIS)114829&fileName=159480061237421.pdf&id=16103&source=NaRDuS&language=srsr
dc.identifier.uri/DownloadFileServlet/IzvestajKomisije159480061237421.pdf?controlNumber=(BISIS)114829&fileName=159480061237421.pdf&id=16103
dc.identifier.urihttps://nardus.mpn.gov.rs/handle/123456789/17976
dc.description.abstractU ovoj tezi razvijen je formalni sistem za dokazivanje teorema incidencije u projektivnoj geometiji. Osnova sistema je Čeva/Menelaj metod za dokazivanje teorema incidencije. Formalizacija o kojoj je ovdje riječ izvedena je korišćenjem Δ-kompleksa, pa su tako u disertaciji spojene oblasti logike, geometrije i algebarske topologije. Aksiomatski sekventi proizilaze iz 2-ciklova Δ-kompleksa. Definisana je Euklidska i projektivna interpretacija sekvenata i dokazana je saglasnost i odlučivost sistema. Dati su primjeri iščitavanja teorema incidencije iz dokazivih sekvenata sistema. U tezi je data i procedura za provjeru da li je skup od n šestorki tačaka aksiomatski sekvent.sr
dc.description.abstractIn this thesis, a formal sequent system for proving incidence theorems in projective geometry is introduced. This system is based on the Ceva/Menelaus method for proving theorems. This formalization is performed using Δ-complexes, so the areas of logic, geometry and algebraic topology are combined in the dissertation. The axiomatic sequents of the system stem from 2-cycles of Δ-complexes. The Euclidean and projective interpretations of the sequents are defined and the decidability and soundness of the system are proved. Patterns for extracting formulation and proof of the incidence result from derivable sequents of system are exemplified. The procedure for deciding if set of n sextuples represent an axiomatic sequent is presented within the thesis.en
dc.languagesr (latin script)
dc.publisherУниверзитет у Новом Саду, Факултет техничких наукаsr
dc.rightsopenAccessen
dc.sourceУниверзитет у Новом Садуsr
dc.subjectČeva/Menelaj dokazi, teorema incidencije, Δ-kompleksi,simplicijalna homologija, formalni sistemi, odlučivostsr
dc.subjectCeva-Menelaus proof, incidence theorem, Δ-complex, simplicial homology,sequent system, decidabilityen
dc.titleFormalni sistemi za dokazivanje teorema incidencijesr
dc.title.alternativeFormal systems for proving incidence resultsen
dc.typedoctoralThesisen
dc.rights.licenseBY-NC-ND
dc.identifier.fulltexthttp://nardus.mpn.gov.rs/bitstream/id/68738/Disertacija.pdf
dc.identifier.fulltexthttp://nardus.mpn.gov.rs/bitstream/id/68739/IzvestajKomisije.pdf


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record