Show simple item record

System for automatic proving of some classes of analytic inequalities

dc.contributor.advisorMalešević, Branko
dc.contributor.otherLutovac, Tatjana
dc.contributor.otherJaničić, Predrag
dc.contributor.otherProtić, Jelica
dc.contributor.otherObradović, Ratko
dc.creatorBanjac, Bojan
dc.date.accessioned2020-11-02T11:21:29Z
dc.date.available2020-11-02T11:21:29Z
dc.date.issued2019-05-24
dc.identifier.urihttp://eteze.bg.ac.rs/application/showtheses?thesesId=7679
dc.identifier.urihttps://fedorabg.bg.ac.rs/fedora/get/o:22866/bdef:Content/download
dc.identifier.urihttp://vbs.rs/scripts/cobiss?command=DISPLAY&base=70036&RID=51815695
dc.identifier.urihttps://nardus.mpn.gov.rs/handle/123456789/17576
dc.description.abstractU okviru ovog doktorata razvijen je sistem SimTheP (Simple Theorem Prover) za automatsko dokazivanje nekih klasa analitickih nejednakosti. Kao osnovna klasa nejednakosti posmatrana je klasa MTP (miksovano trigonometrijsko polinomskih) nejednakosti. U doktoratu su navedene jos neke klase analitickih nejednakosti na koje se, uz odred-ene dodatne korake, moze primeniti prikazani sistem. Za potrebe sistema je kreirano vise originalnih algoritama poput algoritma za trazenje prve pozitivne nule polinomske funkcije koji je baziran na Sturmovoj teoremi, algoritma za trazenje najmanjeg odgovarajuceg stepena aproksimacija Tejlorovim razvojima, algoritma sortiranja aproksimacija i slicnih. Svi algoritmi su prikazani pseudokodom i detaljnim objasnjenjem slucajeva upotrebe. Rad sistema i koriscenih algoritama ilustrovani su na vecem broju konkretnih analitickih nejednakosti od kojih su neke bile otvoreni problemi, a koji su potom reseni metodama sistema i publikovani u renomiranim casopisima. U okviru doktorata dat je detaljan prikaz oblasti i problematike vezane za dokazivanje i automatske dokazivace. Razmotreni su osnovni problemi sa kojima se srecu korisnici vecine automatskih dokazivaca, ali su takod-e analizirani i neki problemi vezani u vezi sa implementacijom automatskih dokazivaca teorema. Razvijena je jedna implementacija sistema SimTheP, a u cilju procene performansi ovog sistema urad-ena je uporedna analiza sa dokazivacem MetiTarski.sr
dc.description.abstractIn this doctoral thesis was developed SimTheP (Simple Theorem Prover), system for automatic proving of some classes of analytical inequalities. MTP (mixed trigonometric polynomial) inequalities were considered as basic class of studied inequalities. Some additional classes of analytical inequalities, on which shown system can be applied with some additional steps, were presented in this thesis. Several original algorithms, such as algorithm for seeking rst positive root of polynomial function based on Sturms theorem, algorithm for seeking smallest appropriate degree of approximation by Taylor series, algorithm for sorting of approximations and similar others, were created for use in system. All algorithms were shown by pseudo-code and detailed use case scenarios. Inner workings of system and application of stated algorithms was illustrated on great number of concrete analytical inequalities, of which some were open problems later solved by methods from system and published in renown journals. In this thesis was also given detailed image of area of research and problematic of theorem proving and automatic theorem provers. Some basic problems with which users of most automatic theorem provers deal were considered, but also some problems of implementation of automatic theorem proving were analysed. One implementation of system SimTheP was developed, and to assess performance of this system, side by side comparison with MetiTarski was conducted.en
dc.formatapplication/pdf
dc.languagesr
dc.publisherУниверзитет у Београду, Електротехнички факултетsr
dc.rightsopenAccessen
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0/
dc.sourceУниверзитет у Београдуsr
dc.subjectautomatsko dokazivanjesr
dc.subjectautomatic provingen
dc.subjectanaliticke nejednakostisr
dc.subjectmiksovano trigonometrijsko polinomske nejednakostisr
dc.subjectanalytical inequalitiesen
dc.subjectmixed trigonometric polynomial inequalitiesen
dc.titleSistem za automatsko dokazivanje nekih klasa analitičkih nejednakostisr
dc.title.alternativeSystem for automatic proving of some classes of analytic inequalitiesen
dc.typedoctoralThesisen
dc.rights.licenseBY-NC-ND
dc.identifier.fulltexthttp://nardus.mpn.gov.rs/bitstream/id/66454/IzvestajKomisije23367.pdf
dc.identifier.fulltexthttp://nardus.mpn.gov.rs/bitstream/id/66453/Disertacija.pdf
dc.identifier.rcubhttps://hdl.handle.net/21.15107/rcub_nardus_17576


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

openAccess
Except where otherwise noted, this item's license is described as openAccess