National Repository of Dissertations in Serbia
    • English
    • Српски
    • Српски (Serbia)
  • English 
    • English
    • Serbian (Cyrilic)
    • Serbian (Latin)
  • Login
View Item 
  •   NaRDuS home
  • Универзитет у Београду
  • Електротехнички факултет
  • View Item
  •   NaRDuS home
  • Универзитет у Београду
  • Електротехнички факултет
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Sistem za automatsko dokazivanje nekih klasa analitičkih nejednakosti

System for automatic proving of some classes of analytic inequalities

Thumbnail
2019
Disertacija.pdf (2.354Mb)
IzvestajKomisije23367.pdf (1.019Mb)
Author
Banjac, Bojan
Mentor
Malešević, Branko
Committee members
Lutovac, Tatjana
Janičić, Predrag
Protić, Jelica
Obradović, Ratko
Metadata
Show full item record
Abstract
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 okv...iru 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.

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 jo...urnals. 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.

Faculty:
University of Belgrade, School of Electrical Engineering
Date:
24-05-2019
Keywords:
automatsko dokazivanje / automatic proving / analiticke nejednakosti / miksovano trigonometrijsko polinomske nejednakosti / analytical inequalities / mixed trigonometric polynomial inequalities
[ Google Scholar ]
URI
http://eteze.bg.ac.rs/application/showtheses?thesesId=7679
https://fedorabg.bg.ac.rs/fedora/get/o:22866/bdef:Content/download
http://vbs.rs/scripts/cobiss?command=DISPLAY&base=70036&RID=51815695
https://nardus.mpn.gov.rs/handle/123456789/17576

DSpace software copyright © 2002-2015  DuraSpace
About NaRDus | Contact us

OpenAIRERCUBRODOSTEMPUS
 

 

Browse

All of DSpaceUniversities & FacultiesAuthorsMentorCommittee membersSubjectsThis CollectionAuthorsMentorCommittee membersSubjects

DSpace software copyright © 2002-2015  DuraSpace
About NaRDus | Contact us

OpenAIRERCUBRODOSTEMPUS