Herbrand's theorem

-

Herbrand's theorem is one of the most important theorems of constructive first order logic: Formula is a tautology if and only if the tautology is some development of Herbrand's formula.

Since each development is a finite formula of the propositional calculus, so it can be settled in finite (exponential) time, the number of Herbrand expansions for the formula is a countable set, which proves each tautology of the first order logic, though it may take an unlimited amount time. Algorithm n = 0; proven = false; while (proven == false) { Y = nre_surfing_Herbrand (X, n); Y '= convert_function_form (Y); if (is_auto (Y ')) proven = true; else n = n + 1; } generate evidence based on Y;

wiki

Comments

Post a Comment

Popular posts from this blog

Association of Jewish handicrafts "Jad Charuzim"

-
The Jewish Handgun Association "Jad Charuzim" - a Jewish craft organization, operating in Galicia since 1875. She was the founder of many synagogues (eg Yad Charuzim Synagogue in Sanok, Jad Charuzim Synagogue in Yaroslav, Zasany Synagogue in Przemysl), burs, self-help and charity activities, libraries, readings and readings. In 1927, in order to enable its members to use small loans, the association established its own credit cooperative "Cooperative Bank of Cooperatives". The Association's activities ceased during World War II. wiki
Read more

Grouping Red Arrows

-
Raggruppamento Frecce Rosse (Red Arrow Group) - Collaborative armed formation of an Italian army composed of Indians, Arabs and Africans during the Second World War. From May to July 1942, an armed formation was formed under the name Raggruppamento Centri Militari, consisting mainly of British Army prisoners of war originating in Arab countries, India and northern and eastern Africa. They were Hindus, Arabs, Sudanese, Tunisians. The officers and the non-commissioned officers were Italian. The formation consisted of three subdivisions: It was about 1.2 thousand. including about 400 Hindus and about 200 Arabs. Colonel Massimo Invrea de Stato headed it. Subsequently, a small number of Tunisians and Indians were sent to Italy to complete their parachute training in Tarquinia. In August 1942, the formation was renamed Raggruppamento Frecce Rosse. After the defeat of the German-Italian forces at El Alamein at the turn of October and November 1942, the Indians and Arabs lost motivation t...
Read more

Catechism of Polish Child

-
Catechism of the Polish Child - one of the patriotic poets Wladyslaw Belzy published in the volume of the Polish Children's Catechism in 1900. The poem is also known under the title "Confession of the Polish Child" or "Catechism of a Young Pole". It starts with the words "Who are you? "Little Pole". His simple form, referring to children's calculations, made him the simplest form of patriotic education of the youngest generation. The work consists of basic questions and answers about the identity features of a young Pole. It made it easier to memorize national characters and symbols. This work was covered in 1951 by censorship in Poland, subject to immediate withdrawal from libraries. wiki
Read more