English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The paper considers the logic calculus of positively constructed formulas (PCF calculus) and based on it automated theorem proving (ATP) method. The PCF calculus was developed and described as a first-order logic formalism in works of S.N. Vassilyev and A.K. Zherlov as a result of formalizing and solving problems of control theory. There are examples of describing and solving some control theory problems, effectively (from the point of view of the language expressiveness and the theorem proving means efficiency) solved using PCF calculus, for example, controlling a group of lifts; directing a telescope at the planet center, which is in an incomplete phase, and mobile robot control. Comparing to the capabilities of other logical means for subject domain formalization and logic conclusion search, the PCF calculus have the advantage of the expressiveness combined with the compactness of knowledge representation, the natural parallelism of their processing, large block size and lower combinatorial complexity of conclusions, high compatibility with heuristics, and great capabilities for interactive proof. The selected class of formulas makes it possible to build constructive proofs. This class of formulas is much wider than the class of Horn clauses used in the Prolog. There are no restrictions in the logical formalization of the axiomatic base of the subject domain, and the target statement is a conjunction of queries (in terms of the Prolog). To test the ATP software system (prover) based on the PCF calculus the authors used the TPTP (Thousands of Problems for Theorem Provers) library. The TPTP format has become a standard in the community that studies automated reasoning. There is a natural need for the developed prover to accept problems in this format as input. Thus, the problem of translating the first-order predicate logic formulas presented in the TPTP format to the POF format arises. This problem is nontrivial due to the special structure of the PCF calculus formulas. The paper proposes a more efficient translation method (compared to the previously developed algorithm in the first implementation of the prover based on the PCF calculus) for the first-order predicate calculus language preserving the original heuristic knowledge structure, and its simplified version for the problems presented in language of clauses. The efficiency is a number of steps and the length of the obtained formulas. The proposed method was implemented as a software system – a language translator of first-order TPTP logic formulas to the PCF calculus language. The paper presents test results of the developed method, which imply that there is a certain class of first-order formulas that are not taken into account as special by existing ATP systems, while the PCF calculus has special strategies that increase the efficiency of the inference search for such class of formulas.

Метод трансляции первопорядковых логических формул в позитивно-образованные формулы