Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people
There are three main families of inference algorithms in first-order logic: direct inference and its application to deductive databases and production systems; backward inference procedures and logic programming systems; theorem proving systems based on the resolution method. When solving specific p...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | Russian |
| Published: |
National Academy of Sciences of Belarus, the United Institute of Informatics Problems
2021-09-01
|
| Series: | Informatika |
| Subjects: | |
| Online Access: | https://inf.grid.by/jour/article/view/1108 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832543448296587264 |
|---|---|
| author | A. М. Sobol E. I. Kozlova Yu. A. Chernyavsky |
| author_facet | A. М. Sobol E. I. Kozlova Yu. A. Chernyavsky |
| author_sort | A. М. Sobol |
| collection | DOAJ |
| description | There are three main families of inference algorithms in first-order logic: direct inference and its application to deductive databases and production systems; backward inference procedures and logic programming systems; theorem proving systems based on the resolution method. When solving specific problems, the most effective algorithms are those that allow you to cover all the facts and axioms and must be taken into account in the process of inference. An example is considered in which it is necessary to prove the guilt of a person in murder. On the basis of statements, a knowledge base is formed from expressions, with the help of which an expression of first-order logic is compiled and proved using direct logical inference. The proof of the reasoning obtained in direct inference using the proof tree is given. However, direct inference provides for the implementation of all admissible stages of logical inference based on all known facts. The article also considers a method based on the resolution when implementing the reverse inference, taking into account the expression obtained in the direct inference. This expression is converted into a conjunctive normal formula using the laws of Boolean algebra and is proved by the elimination of events using the conjunction operation. |
| format | Article |
| id | doaj-art-b9723a203fca469595366fed73c31e10 |
| institution | Kabale University |
| issn | 1816-0301 |
| language | Russian |
| publishDate | 2021-09-01 |
| publisher | National Academy of Sciences of Belarus, the United Institute of Informatics Problems |
| record_format | Article |
| series | Informatika |
| spelling | doaj-art-b9723a203fca469595366fed73c31e102025-02-03T11:40:29ZrusNational Academy of Sciences of Belarus, the United Institute of Informatics ProblemsInformatika1816-03012021-09-011839710510.37661/1816-0301-2021-18-3-97-105981Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of peopleA. М. Sobol0E. I. Kozlova1Yu. A. Chernyavsky2Belarusian State UniversityBelarusian State UniversityBelarusian State University of Informatics and RadioelectronicsThere are three main families of inference algorithms in first-order logic: direct inference and its application to deductive databases and production systems; backward inference procedures and logic programming systems; theorem proving systems based on the resolution method. When solving specific problems, the most effective algorithms are those that allow you to cover all the facts and axioms and must be taken into account in the process of inference. An example is considered in which it is necessary to prove the guilt of a person in murder. On the basis of statements, a knowledge base is formed from expressions, with the help of which an expression of first-order logic is compiled and proved using direct logical inference. The proof of the reasoning obtained in direct inference using the proof tree is given. However, direct inference provides for the implementation of all admissible stages of logical inference based on all known facts. The article also considers a method based on the resolution when implementing the reverse inference, taking into account the expression obtained in the direct inference. This expression is converted into a conjunctive normal formula using the laws of Boolean algebra and is proved by the elimination of events using the conjunction operation.https://inf.grid.by/jour/article/view/1108first-order logicdirect inferencereverse inferencereasoning formationresolution methodconjunctive normal formulaproof tree |
| spellingShingle | A. М. Sobol E. I. Kozlova Yu. A. Chernyavsky Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people Informatika first-order logic direct inference reverse inference reasoning formation resolution method conjunctive normal formula proof tree |
| title | Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people |
| title_full | Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people |
| title_fullStr | Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people |
| title_full_unstemmed | Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people |
| title_short | Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people |
| title_sort | application of first order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people |
| topic | first-order logic direct inference reverse inference reasoning formation resolution method conjunctive normal formula proof tree |
| url | https://inf.grid.by/jour/article/view/1108 |
| work_keys_str_mv | AT amsobol applicationoffirstorderlogictoidentifyorganizersandperpetratorsofillegalactionsinteamsofalimitedcircleofpeople AT eikozlova applicationoffirstorderlogictoidentifyorganizersandperpetratorsofillegalactionsinteamsofalimitedcircleofpeople AT yuachernyavsky applicationoffirstorderlogictoidentifyorganizersandperpetratorsofillegalactionsinteamsofalimitedcircleofpeople |