Találati lista | Tudóstér

001-es BibID:	BIBFORM044149
Első szerző:	Pásztor Varga Katalin (matematikus)
Cím:	Comparison and usability of two rewriting systems for theorem proving / Pásztor Varga Katalin, Várterész Magda
Dátum:	2002
Megjegyzések:	Eötvös Loránd Tudományegyetem - Általános Számítástudományi Tanszék In this paper two rewriting systems for logical formulas are regarded. One of them is suggested by A. Dragálin [1], the other by M. Fitting [2]. Both of them are based on the duality of the logical connectives conjunction and disjunction. By these methods the formulas can be rewritten into disjunctive normal form (DNF) and conjunctive normal form (CNF) to take them usable forthe tableau and for the resolution calculus. The equivalent power of these methods is shown also. As in every step both rewriting methods result a so-called generalized DNF or CNF, it is possible to execute the steps of the theorem proving and rewriting algorithms not separately [4]. We suggest a formula complexity controlled algorithm allowing more powerful usability for these rewriting systems in theorem proving. The pp method [1] handles symbolic dual operations in a general way but therecursive rewriting [2] treats the logical connectives after the unified notation of Smullyan [5]. It seems to be profitable to elaborate an algorithm bringing together the useful properties of both rewriting systems.An algorithm is given which uses the denotation technic of pp rewriting combined with a directed strategy to get into a plus or point normal form. Some simplification is executed during the algorithm and a reduced normal form is obtained.
Tárgyszavak:	Természettudományok Matematika- és számítástudományok idegen nyelvű folyóiratközlemény hazai lapban
Megjelenés:	Pure Mathematics and Applications. - 13 : 1-2 (2002), p. 293-302. -
További szerzők:	Várterész Magdolna (1954-) (informatikus, matematikus)
Internet cím:	Intézményi repozitóriumban (DEA) tárolt változat
Borító:
Saját polcon: