Contents. Annotations.

Introduction to Relational Logic   M.A.Malkov . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
The relational logic is constructed as the integration of classic and computational logics. In classic logic unnatural (NBG) set theory is replaced by natural one. In the theorem proving of computational logic, sentences in A-prenex form with Scolem functions are replaced by sentences in AE-prenex form without unnatural functions (A is the symbol of universal quantifier, B is a symbol of existential quantifier). This allows to replace induction by the computer-oriented rule of finite descent. In the logic programming of computational logic, the ghost effect is removed. This allows to solve the negation problem.

The term "relational logic" appeared from the term "relational calculus", introduced by E.Codd. His term differs from the term "predicate calculus" by presentation of functions as relations, because relations are simpler for computer processing than functions.
But it means terms are absent and an atom (atomic formula) is present syntactically as a relational symbol with argument places filled by variable symbols.
Usage of atoms without terms complicates logical formulas. So the terms are introduced to shorten the record of formulas. And it appears, the terms can be created not only by functions, but by predicates too (predicates has no functional dependence of arguments).
The term "computational logic" was introduced by J.A. Robinson. One problem of this logic is theorem proving. In this logic all formulas must be present as disjunctive clauses, in Scolem form without quantifiers. The valid formulas must be absent in this form. Any subset of formulas, presented as disjunctive clauses, creates an axiom set of a theory. These axioms can also be theorems and definitions. The basic inference rules are the resolution (computer analog of modus ponens) and paramodulation (computer analog of equality axioms).
Now the generalized clauses are used. They consist of one (or nil) disjunctive clause and some conjunctive clauses. All these clauses are joined by disjunctions. The members of conjunctive clauses are joined by conjunctions and have variables bound by existential quantifiers. These quantifiers are implicit and mean in beginning of every conjunctive clause. There are conjunctive clauses consisted of one literal (a literal is an atom with or without negation).
The generalized clause is constructed from an AE-prenex sentence without Scolem functions. The quantifiers are absent in the generalized clause, but variables, bound by universal quantifiers, are denoted by x_i (i is a natural number), variables bound by existential quantifiers are denoted by a_i.
As an exception the generalized clause can be constructed from an EA-prenex sentence and variables bound by existential quantifiers are denoted by c_i.
This generalized clause is used for theorem proving and called the first normal form. Inference rules for the generalized clause are called the generalized resolution and generalized paramodulation.
The generalized clauses are irreplaceable for using the induction rule. The computer analog of the induction rule is called the finite descent and the computer analog of infinite descent is called the generalized finite descent.
The other part of the computational logic is the logic programming, created by A. Colmerauer. One problem of it is a model construction for a theory.
In this part of the logic all formulas must be positive definitions of notions in the AE-prenex sentences. From these sentences the second normal form is constructed.
The second normal form is back implication "<-" with a defined atom in the left part and a defining formula in the right part. The defining formula are present in conjunctive clause form, i.e. as a set of literals, joint by conjunctions. The defining formula must be not valid one.
One more problem is a construction of all models, i.e. a set theory. We accept that all models are numerical and can be got from the set of the natural numbers and from a finite number of operations of the direct product and power set. This theory is consistent.
The last part of the computational logic is the finite logic. This logic is created to construct theories (knowledge bases) and their constructive models (data bases) by using computer calculations. At non-monotone calculations we use the standard 4-valued logic and this logic lets resolve the negation problem. The standard 4-valued logic is used only during the calculations. Finishing the calculations we return to the 2-valued logic.
The main problem of the finite logic is the high effectiveness of calculations.
The integration of the classic and computational logics allows to perfect the latter. So the integration with the classic logic allows to cut off rather vast investigations that are wrong or unimportant.

Relational Propositional Logic  M.A.Malkov. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
Propositional logic consists of the theory calculus, i.e. the construction of all zero order theories, and the axiom calculus, i.e. the construction of all axioms of a theory. But these calculi belong to the set of the first order theories.

All zero order theories and their axioms are present as disjunctive clauses. These clauses are deduced from the conjunctive normal form. The valid formulas are removed.
In the first calculus all consistent theories are constructed over set of 5 atoms. A number of these theories equals 4 10⁹, but non-automorphic (over the literal set) theories are only 10⁶. Further classification of these theories are given.
In the second calculus three problems are decided: discovery of inconsistent theories (for theorem proving), closure of theories and construction of all systems of independent axioms for a theory.
All rules (algorithms) of the decision of the problems in both calculi have effectiveness unmatched with existing rules.

Relational Logic and Arithmetic  M.A.Malkov. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
Four axioms of the natural numbers are present: the successor function is injective, 0 is not anyone's successor, the order is natural and there is no number between every number and its successor. Valid formulas are not included in axioms. The induction rule is substituted by the finite descent.
The other numbers constructed by inversion of the fast increasing function of order n. The integers are constructed by inversion of the fast increasing function of order 1. The rational numbers are constructed by inversion of the fast increasing function of order 2. The fast increasing function of order 3 has two inverse functions used to construct numbers called as radicals and logarithms. There are arithmetic numbers of order 4 and more.

Axioms of Classic Set Theory  M.A.Malkov. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
The axioms of classic set theory NBG are divided into axioms of one-place classes and axioms of multi-place classes. These axioms are present in the first normal form too and so become the program ready for execution.

Functional Extension of Language C++. I. IF and BREAK Statements. VOID and CLASS Types  M.A.Malkov. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
The syntax extension of language C++ is given by reducing statements of the language to operations. The conditional operation is expanded and the statement "break" is overloaded. It allows to eliminate the statements "if", "for", "while", "do", "go to", "try", "throw" and "catch". As a rule any operation with any argument "void" has value "void".

The set of postfix operations of assignment is extended. Any operation used in the prefix form can be used in the postfix form too. In particular, the operation of adding can be used in two forms "+=" and "=+".
The syntax and semantics of type "class" is extended. This type can incapsulate not only functions, but also all data types processed by these functions. It allows to eliminate the specification "friend" and the pointer "this".

Relational Programming  M.A.Malkov. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
Relational programs consist solely of procedures (relations). The functions are used only to calculate values of arguments (actual parameters). These functions belong to a fixed set and are used to construct terms. Relations are used to construct logical formulas. A program is defined as a set of logical formulas. This set can be used to construct theories (knowledge bases, if every knowledge is formalized by logical formulas) or models (data bases) of these theories.

As a rule theory construction is reduced to theorem proving, i.e. proving that some problem has a solution based on existing knowledge.
At data base constructing the relational tables are calculated with help of logical formulas. These formulas are definitions of relations corresponding to calculated tables. Every definition is interpreted as a sequence of intersections, joints, projections and direct products of the source tables. At calculation an abstract computer is used. This computer has no memory. So the way of table presentation into a computer or in a computer net are ignored.
The theory constructing is illustrated by the example of equivalential calculus, and the model constructing is illustrated by the example of rule of sequential removing of atoms in inconsistent theories.