Interactive generation of new knowledge based on automatic means of logical inference

The work relates to the field of knowledge representation and algorithmization of their processing. To describe the subject of consideration by a set of statements and their processing, logical means of the first order type are used. Unlike the well-known achievements in the field of automatic proof (AP) in formal axiomatic theories, the automatic text synthesis of statements is complicated by the poor formalizability of the value of knowledge concept contained in the text. Based on the development of the calculus of positively-formed standardized formulas (pfs-formulas) the possibilities of analysis automation of the description of the subject matter and interactive generation of meaningful statements to improve this description are investigated. The proposed method of interactive knowledge generation integrates the capabilities of AP with algorithmized human-machine synthesis of new knowledge texts. AP in the calculus of pfs-formulas helps a person not only in the analysis of properties, but also in the choice of the required properties of the description of the subject matter. When the absence of a property desirable for a person in the analyzed knowledge is revealed by means of AP, the hypotheses is formed that logically guarantees the presence of the required property. Variants of hypotheses are automatically synthesized in a preliminary form, which are then refined interactively to improve the content of the generated text of new knowledge. The rules of synthesis are justified. Their application continues the inference in situations of inapplicability of the basic rule of inference in the calculus of pfs-formulas. The extension of calculus by the rules of synthesis transforms it as a first-order calculus of the deductive type into a means of deductive-abductive inference, which differs from the known works using abduction by the absence of a number of restrictions. Illustrative examples demonstrate the representation, analysis and generation of knowledge. These examples also show in interactive knowledge processing the importance of visualization of the processed text, provided by the large-block structure of pfs-formulas constructed from typical quantifiers. In conclusion, the results of the paper and possible directions for the development of the results are formulated.