Celem tej pracy jest zbadanie ograniczenia górnego na procedurę iteracji w dół w programach w Prologu. W głównej części pracy pokazujemy schemat konstrukcji programów, które iterują się przez a kroków, dla każdej rekurencyjnej liczby porządkowej a. Następnie używamy notacji porządkowej Kleene'go, aby skonstruować program iterujący się przez dokładnie ωC−K kroków. Ostatnia część głównej sekcji pracy pokazuje ograniczenie górne na iterację w dół - ωC−K. Dowód opiera się na ograniczeniu na ekspresywność definicji induktywnych, które mogą być reprezentowane jako pewne formuły arytmetyczne. W ostatniej części pracy badamy liczby porządkowe iteracji w dół dla programów Prologa, których klauzule nie posiadają operatora koniunkcji - ograniczone programy. Pokazujemy ograniczenie górne na ograniczenie programy, w których występują jedynie unarne predykaty. Prezentujemy kilka narzędzi ,powstałych w procesie próby dowodu, że ograniczenie na liczby porządkowe iteracji w dół ograniczonych programów to ω^ω - hipoteza na końcu tej pracy.

The aim of this document is the examination of the upper bound on downwarditeration procedure in Prologue programs. In the main section of this documentwe provide a schema for the construction of programs that downward iterate forexactly α steps, where α is any recursive ordinal. Later, we use Kleene’s ordinalnotation to construct the program which iterates for exactly ωC−K steps. Thelast part of the main section provides an upper bound on any downward ordinal for Prologue program - ωC−K. It is based on the bound on the expression strength of inductive definitions that might be represented as some arithmetical formulas. In the last section of this document we are studying downward ordinals forPrologue programs such that their clauses do not contain conjunction operator- limited programs. We give an upper bound on limited programs with onlyunary predicates. We also present a couple of tools that were created while attempting to prove that the upper bound on the downward ordinalfor all limited programs is ω^ω - conjecture at the end of this paper.