Naslov
Domain dependencies of automated theorem proving resolution strategies

Autori
Bogunović, Nikola ; Jurinac, Robert

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the MIPRO '97 Symposium : Microelectronics, Electronics and Electronic Technologies / Biljanović, Petar ; Skala, Karolj ; Ribarić, Slobodan ; Budin, Leo - Rijeka : Hrvatska udruga za informacijsku i komunikacijsku tehnologiju, elektroniku i mikroelektroniku - MIPRO, 1997, 167-170

Skup
MIPRO '97, 20th International Convention

Mjesto i datum
Opatija, Hrvatska, 19.05.1997. - 23.05.1997

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
artificial intelligence; automated reasoning; theorem proving

Sažetak
The choice of computation rule in automated theorem proving systems has a great bearing on the size and structure of the corresponding search space. A number of strategies have been proposed to reduce the size of the resolution graph. However, the choice of the particular strategy, with respect to the domain of application, is still an open question. The paper reports on the results of an empirical study, that sought to establish the degree of correlation between various problem domains and known resolution strategies. A number of problems from the mathematical domain, logical puzzles, and natural language analysis, were investigated with breadth-first, depth-first, set of support, and Prolog strategies. The results, validated on several distinct theorem provers, indicate strong strategy preferences.

Izvorni jezik
Engleski

Znanstvena područja
Elektrotehnika

POVEZANOST RADA