Naslov (srp)

Sistem za automatsko dokazivanje nekih klasa analitičkih nejednakosti

Autor

Banjac, Bojan, 1987-, 33371751

Doprinosi

Malešević, Branko, 1965-, 12692839
Lutovac, Tatjana, 1966-, 33783911
Janičić, Predrag, 1968-, 12760935
Protić, Jelica, 1962-, 25654631
Obradović, Ratko, 1965-, 13235303

Opis (eng)

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.

Opis (srp)

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.

Opis (srp)

Elektrotehnika i racunarstvo - Primenjena matematika / Electrotechnics and Computer science - Applied mathematics Datum odbrane: 24.05.2019. null

Jezik

srpski

Datum

2019

Licenca

Ovo delo je licencirano pod uslovima licence
Creative Commons CC BY-NC-ND 2.0 AT - Creative Commons Autorstvo - Nekomercijalno - Bez prerada 2.0 Austria License.

http://creativecommons.org/licenses/by-nc-nd/2.0/at/legalcode