The relational logic is an extension of the classic logic. A part of the relational logic is the natural relation logic. The elegant but unnatural classic set theory is replaced by the most natural set theory. In the natural set theory the family of all countable ordinals is countable.
Relational logic and arithmetic of real numbers. Non-standard analysis. M.A.Malkov . . . . . . . . . . 6
Arithmetic of real numbers is constructed on base of Cantor model. Continuity determinates on base of relational logic. Arithmetic of hyperreal numbers is constructed on base of Cantor model, too. Relational logic is used to determinate hyperextension, increments and differentials. Transfer principle, evaluation of indeterminate forms, integrals, Taylor series and replacement of sum by integral are stated more natural.
Real numbers are defined as left half-infinite open intervals of rational numbers. The set of these intervals forms standard model of real numbers. It is extension of Cantor model for real numbers. Operations of the sum and product, the constant 0 and 1 are defined. Implementation of all axioms of the field of real numbers is shown. Embedding of natural and rational numbers in this field is defined.
Definition of continuous relations is entered by using topology in Euclidean space Rn. Relations are considered as a variety, which maps are functional dependences.
Further, hyperrational numbers is introduced as extension of the field of rational numbers by adding the new rational number delta, indefinitely close to 0. Such extension is the field of rational functions of delta. The infinitesimal hyperreal numbers are defined as left open intervals of infinitesimal hyperrational numbers. The positive infinite hyperreal numbers are defined as left open intervals of positive infinite hyperrational numbers. Then the other hyperreal numbers are defined. It is shown the standard model of hyperrational numbers is a subset of N2 P (N5). The external hyperreal numbers are defined. A number of them are uncountable and between two arbitrary hyperreal numbers there are external numbers. The associative low does not
hold for external numbers so they are excluded from hyperreal axis. The natural and rational numbers are embedded into the field of hyperreal numbers. Constants 0, 1, delta, the arithmetic operations and the relation of order are determined for hyperreal numbers. All axioms of the field of rational numbers hold except the axiom of continuity for the hyperreal axis. But Archimedean principle holds if hypernatural numbers are used.
The equivalence relation ``to be near'' is introduced. This relation forms equivalence classes. Except two classes, each equivalence class contains one real number and all hyperreal numbers near real. Two classes contain all infinite hyperreal numbers. One class contains numbers near -infty, the other class contains numbers near +infty. This more convenient with respect to the Robinson theory.
Hyperextension of the real relations is determined. Each isolated point in the relation remains without changes, each point that is limit in the given direction of Euclidean space is replaced by an interval of hyperreal axis such that this interval is placed in the given direction and contains the equivalent class for the limit point. All this provides the uniqueness of hyperextension. The hyperextension is an operator, and has the inverse operator of standard part.
The transfer principle is investigated. The same logic formulas hold in the arithmetic of real and hyperreal numbers if all definitions are correct. In particular, the definition of continuity is not correct in the arithmetic of hyperreal numbers, the hyperextension of some functions can be continuous though these functions does not continuous. The Dirichlet function becomes not a function at the hyperextension. So the transfer principle must be used with accuracy.
The evaluation of indeterminate forms are stated as term calculations when a term becomes not computed at some points, but after execution of hyperextension at 0 to infinitesimal delta, transformation and standard part, this term becomes computed.
Then the infinitesimal constant delta is defined as an independent axis component of infinitesimal vectors. Infinitesimal vectors are used to determinate directions. Directions are considered as vectors of 0 length. Each direction has axis components if the length of directions is an infinitesimal value instead of 0.
Increments and differentials are defined for relations. Increments are considered as a vector that begins and ends at points of relation. Axes components of this vector are the independent and dependent increments. When independent increments tend to delta the dependent increments become hyperreal. The independent increments become the differential with respect to the independent axis, the linear part of dependent increments becomes the differential with respect to the dependent axis. I.e., the independent differential is a constant and equal to delta.
When relations can be present as variety with maps, then the increments and differentials of functions arise. The differentials of functions replace the dependent differentials.
The definite integrals are determined as an infinite sum of products of delta and integrand value at every point. It extends the Lebesgue definition on hyperreal values.
The non-standard methods of analysis, developed by Leibniz and used by Taylor, are applied to construction of the infinite Taylor series, the Euler-Maclaurin formula, infinite sums, O and o-estimations, forms with indeterminacy etc.
Definability and computability M.A.Malkov . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
In the article definability is set by the first normal form of relational logic. Computability (the algorithm theory) is set by the second normal form (the logic programming). This form replaced natural algorithms and Turing machines and does not depend on model in which relations are interpreted. It is shown, that semi-group with one defining relation is solvable, if the left part of this relation has no identical beginning and end.
The article consists of three parts.
The first part is devoted to definability of relations.
It is marked that in any theory there are indefinable and definable relations. Properties of indefinable relations are set by the basic axioms of the theory, properties of definable relations are set by definitions.
The notion is definable if it is the relation, and this relation is the left part of definition, and the right part is a formula of logic of any order. The left and right parts are divided by the symbol of logic equivalence.
Each definition disjoints on positive and negative.
In the positive definition the symbol of logic equivalence is replaced with the return implication. The return implication is presented by the arrow directed to the left: "<-".
In the negative definition the symbol of logic equivalence is replaced by usual implication, or replaced by return implication but then the left and right parts of the definition are added by negation.
The positive definition is used for construction of models of a theory, the negative definition is used for construction of complement of these models.
The first normal form is entered for representation of the positive and negative definitions. This form allows to remove ambiguity of definitions by presentation in AECNF, i.e. in the prenex conjunctive normal form with universal quantifiers before existential quantifiers. Then all quantifiers are removed.
The first normal form is very convenient for the automatic proof of theorems of the theory.
The second part of the article is devoted to the computability of relations.
Under computability it means the construction of a model of a theory on the abstract computer with the non-limited resources. Under computability of a relation it means the construction of the set interpreting this relation in the given model of the given theory (on the same computer).
The relation is computable even if the appropriate set is infinite. But infinite work of the computer is not allowable. So the basis of computability is the approximation calculus. The computability consists of steps, and each new step (or a group of steps) allows to increase accuracy of calculations. It is possible to calculate infinite objects, in particular, the infinite sets through approximation by the finite sets. The other examples of infinite objects are irrational numbers, integrals etc.
The computability and definability have a close connection. The definition of the relation in the second normal form is a program ready for performance on the abstract computer. It means, the program does not depend on a model of the theory. But the result of performance of the program depends on a model.
The definition of the relation is computable if the second normal form contains only computable negations. If the negations are not computable, it is necessary to search for other definition of the relation or to use the standard 4-valued logic, allowing to calculate even non-computable negations. This logic can be used if the relation is computable, i.e. there is a definition with computable negations, but this definition is difficult for finding.
Instead of Turing machine the relational computer is used. This computer executes programs in the first and second normal form. For the second normal form, rules of calculation of conjunctions, negations, existential quantifiers and return implications are formulated. Calculation of universal quantifiers is replaced by calculation of negation of existential quantifiers. The ghost effects (by-effects) and ways of their overcoming are stated. For non-monotonic calculations the relational computer uses 4-valued logic.
The third part of the article is devoted to the word problem in semi-groups.
The order in semi-groups is entered. For semi-groups with some defining relations, any class of equivalence is presented with order of subsets.
The semi-groups with one defining relation is investigated in details. It is shown the word problem is solvable in the semi-groups with one defining relation if left part of this relation is non-crossed (i.e. has no identical beginning and end).
High order logic. M.A.Malkov . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
The second order logic is presented by syntactic and tabular means. This logic differs from the first order logic only by presence of quantifiers for relation and theory variables.
The second order logic is intended for construction of theories of the second order and models of these theories. One of theories of the second order is the first order logic. This article is devoted basically to construction of the first order logic by means of the second order logic. There are two ways of such construction, one is syntactic and other is tabular (or relational).
The syntactic way is based on the alphabet which letters are used to construct formulas of theories. There are an alphabet for theories of the first order and an alphabet for theories of the second order. Both alphabets are infinite and contain symbols of sorts.
The sort is a special relation and interpreted as a set of values of the appropriate variables. The variable is interpreted as arbitrary member of this set.
Formulas of the second order logic use both alphabets. Distinguishing letters of these alphabets, we place a point above letters of the second alphabet. This point can be absent only in specially stipulated cases.
The construction of the second order logic differs from the construction of the first order logic little. The basic difference consists of explicit and implicit quantifiers of the second order, in particular, of quantifiers on a set of the first order relations. In the rest, theories of the second order are similar to theories of the first order.
The tabular way of theory construction has nothing common with syntactic way. There is no alphabet and syntax of statements in this alphabet. Tables consist of lines and columns, elements of tables (on crossing of a line with a column) are natural numbers. In tables there are no logic symbols and delimit symbols. All formulas are presented in the parenthesis-free record. Therefore, the structure of tables for theories of the first and second order completely coincides. Difference only in the name of tables. This difference is similar to difference of two alphabets in syntactic variant when letters of alphabets are marked or are not marked by a point above letters.
Functional extension of C++.II M.A.Malkov . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
The new language fC++ is introduced. This language is a functional extension of C++. Every statement of C++ must have a value, even empty. The new type of variables is added such that the values of these variables are types. The new technique of automatic memory allocation is offered.
This article continues the article of the previous issue.
The use of labels is strictly limited. Only "break" can use labels, and these labels must be located after "break". The marked statements must be in the same block with "break" or immediately after block that contains "break" or a function call with "break" in the body of this function. So "break" realizes arbitrary interruption, including exceptions, and programs remain structural. But the labels can be functions, and this allows to transfer information at interruptions. Besides, the labels can form arrays.
The new specifier var allows to use the numbers of unlimited length. The length of the data with the specifier var is variable: some bytes specify length of the data in bytes, the others bytes contain the data itself.
The types rational, real and complex are introduced for computational algebra.
The automated distribution for all structures of memory is offered.
If the object is a table, then the special variable is added in the first index at the declaration. This variable always equals the number of lines in the table. Before initialization this variable has value 0. The maximal value of the first index can be pointed or not. If the maximal value is not pointed, then this value is calculated automatically at the first initialization. But in both cases the actual value can be more than maximal. Using the information on the speed of filling of memory, the computer can predict real volume of necessary memory and requires the additional memory of the more real volume.
Such structures need no pointer. In particular, the string of characters must be defined as a character array, i.e., as a table with one index.
The sequence of statements works out a value, too. If the sequence is parenthesized, then the value of this sequence equals the value of the last statement. But the parentheses are overloaded, and there are exceptions of this rule. If the sequence is braced, then the value of this sequence is the sequence of values of each statement.
If the sequence of statements has a semicolon as the delimiter, then these statements are executed strictly in the sequence of their order. If the sequence of statements has a comma as the delimiter, then these statements are executed in the sequence of arbitrary order. This can be used for the parallel execution.
The new type is offered. This type, named type, is for variables if value of these variables is a type.
The type Report is placed in the standard library. This type is intended for the fast drawing up of the report on the basis of an inquiry.
Artificial intelligence and theorem proving M.A.Malkov . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
Problems of artificial intelligence are considered on example of automated theorem proving.
Two ways of construction of artificial intelligence are considered. The first way demands development of very big number of programs which realize functions of natural intelligence, and also use deduction and induction for processing of accumulated experience in a knowledge base. The deduction extract necessary information from a knowledge base, the induction fills up a knowledge base. Other way demands the minimal number of the programs to realize functions of training and self-training. But process of training and self-training may demand decades for accumulation of necessary knowledge. Problems of artificial intelligence are illustrated on the example of strategy for construction of a proof tree in sentential calculus. We consider two variants for construction of binary resolution proof tree, in down and breadth and one variant for construction of direct proof tree.
Automated theorem proving and logical modelling S.V.Popov . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
We replace logical formulas by programs and search of proofs by construction of fixed point of these programs. It means we use operational semantics instead of syntactic transformations.
Some approaches to the problem of automation of theorem proof are described. The attempt is made to allocate the various concepts which have arisen in this direction is undertaken to formulate typical difficulties for them. As the problems of the automated acceptance of decisions is traditional for artificial intelligence, such analysis of existing approaches has not only theoretical, but applied value, too.
The most traditional approach in automation of proofs is syntactic. For the purposes of the automatic proof we use various logic calculi, which inference rules remind the natural substantial deduction. In the article we describe such calculus which inference rules easily give the substantial interpretation. This calculus allows to describe the kind of deduction, which is close to substantial deduction.
On its example we demonstrate the main difficulty which should be overcome at automation of reasoning. The formal means, which would seem natural from the point of view of substantial reasoning, always allow to receive the big number of the formulas, which have no unequivocal substantial interpretation. A typical example is the formula "from false everything follows", which is true in classical logic, but in substantial reasoning is used only under certain conditions.
In the article the description of a number of strategies is given with demonstration by the appropriate examples.
As opposition to the syntactic approach at automation of proofs in the article we give the semantic concept of the decision of this problem. The essence of it consists in the following. Each problem is formulated in conceptual basis of subject domain to which it belongs. It means each problem presents the logic formula establishing connection between these concepts of the basis. If the problem has a decision, then it has logical model, in which the decision is a set of relations (i.e., basic concepts). Construction of such model is carried out with the help of so-called operational semantics for logic formulas. This semantics is formulated as follows. Each formula of the first order at the certain treatment may represent itself as the program for construction of own model with the finite carrier. In other words, each formula has both logic semantics and operational semantics. Operational semantics has property of completeness: each formula is a program and each fixed point of the program is logical model for this formula, and otherwise, each logical model of any formula is a fixed point of the program constructed under this formula.
In result, the transformation of the formula for the initial problem in the program gives means of the decision of this problem. But by virtue of universality this method has all lacks, which are available for syntactic methods, i.e., big sorting out at finding fixed points. For overcoming this difficulty we use other way instead of the traditional approach of use of various strategy of search. It bases on the interpretation of received decision in concepts of the subject domain, i.e., this decision is substantially meaningful. Therefore for the description of problems we give the formal language, rich enough to describe complex problems, but natural from the point of view of substantial deduction. This language is described in the article, and we prove completeness of operational semantics relative to logical.
Realization of logical modelling system is a system of two-level programming. The first level is logical, it serves for the description of a subject domain, the second is operated, it is used for the formulation of strategy of search. Both levels are realized as programming languages, the first language is logic, the second is operational, which serves as a meta language relative to the first. For illustration of opportunities of the system, we give the program and the decision of well-known problem for the eight queens.