Title
Sistem za automatsko dokazivanje nekih klasa analitičkih nejednakosti
Creator
Banjac, Bojan, 1987-, 33371751
Copyright date
2019
Object Links
Select license
Autorstvo-Nekomercijalno-Bez prerade 3.0 Srbija (CC BY-NC-ND 3.0)
License description
Dozvoljavate samo preuzimanje i distribuciju dela, ako/dok se pravilno naznačava ime autora, bez ikakvih promena dela i bez prava komercijalnog korišćenja dela. Ova licenca je najstroža CC licenca. Osnovni opis Licence: http://creativecommons.org/licenses/by-nc-nd/3.0/rs/deed.sr_LATN. Sadržaj ugovora u celini: http://creativecommons.org/licenses/by-nc-nd/3.0/rs/legalcode.sr-Latn
Language
Serbian
Cobiss-ID
Theses Type
Doktorska disertacija
description
Datum odbrane: 24.05.2019.
Other responsibilities
mentor
Malešević, Branko, 1965-, 12692839
član komisije
Lutovac, Tatjana, 1966-, 33783911
član komisije
Janičić, Predrag, 1968-, 12760935
član komisije
Protić, Jelica, 1962-, 25654631
član komisije
Obradović, Ratko, 1965-, 13235303
Academic Expertise
Tehničko-tehnološke nauke
University
Univerzitet u Beogradu
Faculty
Elektrotehnički fakultet
Alternative title
System for automatic proving of some classes of analytic inequalities
Publisher
[B. Banjac]
Format
158 listova
description
Elektrotehnika i racunarstvo - Primenjena matematika / Electrotechnics and Computer science - Applied mathematics
Abstract (sr)
U 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.
Abstract (en)
In 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.
Authors Key words
automatsko dokazivanje; analiticke nejednakosti;
miksovano trigonometrijsko polinomske nejednakosti
Authors Key words
automatic proving; analytical inequalities;
mixed trigonometric polynomial inequalities
Classification
510.26:517.518.83:004.8(043.3)
Type
Tekst
Abstract (sr)
U 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.
“Data exchange” service offers individual users metadata transfer in several different formats. Citation formats are offered for transfers in texts as for the transfer into internet pages. Citation formats include permanent links that guarantee access to cited sources. For use are commonly structured metadata schemes : Dublin Core xml and ETUB-MS xml, local adaptation of international ETD-MS scheme intended for use in academic documents.