О возможности цифровизации и компьютерной верификации версий в процессе расследования

Аннотация

A complex and important task in the process of investigating criminal cases is the iterative procedure of putting forward a version, checking it for consisten- cy and identifying logical consequences relevant to the goals on its basis. The paper substantiates the possibility of constructing a digital logical – semantic model for the current state of the investigation, using formulas from atomic statements of universal syllogistics (multivalued logic)L .A computer program for verification of logical con- S 2 sequence allows you to check whether there is a logical consequence from the infor- mation available at this stage of the investigation. L syllogistics differs from many S 2 well – known syllogistics in the ability to express single – meaning statements by means of a conjunctive formula. The program also allows you to visually depict the logical connections of L statements in the form of a discrete Venn diagramConstructions and S 2 calculations in the digital model of logical relations can be used in any field of activity in cases when it is necessary to find out what follows from the logical relations of objects that make up the digital model of the subject area of activity.The digital model under consideration can be successfully used for the formation and debugging of instructions regulating activities. Keywords: process of investigating criminal cases, digitalization of logical -se- mantic models, syllogistics, applications of logic, decision-making, verification of log- ical consequence Процесс расследования состоит в разрешении проблемных ситуаций путем итерационного процесса выдвижения версий, согласованных с имеющейся на данном этапе информационной базой. Обновление информационной базы зача- стую приводит к изменениям плана расследования и может сделать текущую вер- 299 Мультидисциплинарные (неюридические) аспекты цифровой трансформации Мультидисциплинарные (неюридические) аспекты цифровой трансформации Multidisciplinary (Non-Legal) Aspects оf Digital Transformation Multidisciplinary (Non-Legal) Aspects оf Digital Transformation сию противоречивой. Сложной и важной в этом творческом процессе является процедура проверки версии на непротиворечивость и соответствие фактологии и отношениям, имеющимся в информационной базе (ИБ). Версия и логические следствия из нее должны логически следовать из фактов и отношений ИБ. «С ло- гической стороны проверка версии (так же, как и проверка научной гипотезы) за- ключается выведении из нее логических следствий и затем в подтверждении либо опровержении их.» (8. С. 104). В работе показано, как можно установить (верифицировать) логическое сле- дование, используя верификацию логического следования в семантическом смыс- ле в цифровой модели (ИБ) в форме суждений универсальной силлогистики. Построение и расчеты цифровой модели логических отношений может ис- пользоваться в любых областях деятельности в случаях, когда необходимо выяс- нить, что следует из логических отношений объектов, составляющих цифровую модель предметной области (ПОД), а также для формальной проверки на дости- жение целей регламентов деятельности. Для цифровизации логико-семантических моделей ПОД выявления и вери- фикации логического следования в семантическом смысле построена универсаль- ная силлогистика (многозначная неклассическая логика) L , правильно построен- S2 ные формулы (ППФ) которой принимают значения в виде одного либо семейства конечных конституентных множеств, состоящих из неотрицательных целых чи- сел. В L указан способ установления семантического следования между правиль- S2 но построенными (ППФ). Атомарные суждения L есть утверждения (1) S2 NOB = A(X,Y),Eq(X,Y),IO(X,Y),X ⊂U,X =U , (1) S Вместо Х и Y можно подставить любые ППФ F (X ),F (X ) алгебры мно- 1 n 2 n жеств. Равносильности (2) выражают семантику трех первых атомарных суждений. A(X,Y)≡(X ⊂Y)⋅(X ⊂U)⋅(X '⊂U)⋅(Y ⊂U)⋅(Y'⊂U), Eq(X,Y)≡(X =Y)⋅(X ⊂U)⋅(X '⊂U)⋅(Y ⊂U)⋅(Y'⊂U), (2) IO(X,Y)≡(X ⋅Y ≠U)⋅(X ⋅Y'≠U)⋅(X '⋅Y ≠U)⋅(X '⋅Y'≠U). Далее точка, знаки «плюс» и «штрих» означают для множеств операции пе- ресечения, объединения и дополнения до универсума, а для булевых перемен- ных – конъюнкцию, дизъюнкцию и отрицание. На русском языке первое суждение выражается как «Все элементы множе- ства Х являются элементами Y, но не наоборот», либо «все элементы объема по- нятия (термина) Х входят в объем понятия (термина) Y и пересечение Х´·Y есть непустое множество». С точки зрения логического следования А(Х, Y) равносиль- но утверждению ∀å∈U[(e∈X) (e∈Y)]·[(e∈Y) (e∈X)] для непустых и не уни- версальных множеств. Eq(Х, Y) – утверждение о совпадении непустых и не универсальных мно- жеств X и Y, при этом ∀e∈U[(e∈X) (e∈Y)]·[(e∈Y) (e∈X). 300 Мультидисциплинарные (неюридические) аспекты цифровой трансформации Multidisciplinary (Non-Legal) Aspects оf Digital Transformation IO(X,Y)≡(X ⋅Y ≠∅)⋅(X ⋅Y'≠∅)⋅(X '⋅Y ≠∅)⋅(X '⋅Y'≠∅)выражается на рус- ском языке словами «X и Y – независимые термины (множества)». Это означает, что межу ними и их дополнениями нет отноше