Development of a prototype solver for extended step theories of propositional logic

Nowadays, there are active researches on the possibilities of using non-classical logics in modeling the cognitive agent's reasoning. The paper considers the problem of developing and implementing a prototype of an Extended Step Theory solver (EST) in the case when decisions on managing a complex technical object are made under strict time constraints. The authors consider a logical system based on using step theories with two types of negation, such systems are called EST. The use of two types of negation allows deducing both unbiased facts and belief facts, which is important when modeling human reasoning. The paper focuses on the issue of organizing the inference procedure based on using non-classical logics in modeling the reasoning of a cognitive agent. There are the main stages of the development of the EST prototype using the propositional logic literals given. There are also descriptions for each solver component, its functions, tasks, input and out-put data. The authors is justify the choice of the clingo output system supporting the formation of extended logic programs Answer Set Programming (ASP) as a tool for implementing the solver. The paper gives the algorithms of translating the EST into a logical program corresponding to the ASP syntax. When organizing logical inference, the authors used the algorithm of cyclic processing of EST belief sets in the clingo environment. The main stages of this algorithm are considered by an example that analyzes the solver's operation stages and the presents the results in the clingo syntax. An example of the solver's work demonstrates the main EST features in hard real-time problems, such as the rejection of logical omniscience, self-knowledge and temporal sensitivity. It is planned further to consider the applicability of the created solver to a more complex formal system – the logic of first-order predicates.