Non-clausal Multi-ary alpha-Ordered Linear Generalized Resolution Method for Lattice-Valued First-Order Logic

2015 ◽  
Author(s):  
Hairui Jia ◽  
Yi Liu ◽  
Yang Xu
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Resolution Method ◽  
First Order ◽  
Generalized Resolution

scholarly journals Application of first-order logic to identify organizers and perpetrators of illegal actions in teams of a limited circle of people

Informatics ◽  
2021 ◽  
Vol 18 (3) ◽  
pp. 97-105
Author(s):  
A. М. Sobol ◽  
E. I. Kozlova ◽  
Yu. A. Chernyavsky
Keyword(s):  
Production Systems ◽  
Order Logic ◽  
First Order Logic ◽  
Logical Inference ◽  
Direct Inference ◽  
Resolution Method ◽  
First Order ◽  
Inference Algorithms ◽  
Reverse Inference ◽  
Normal Formula

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.

Sign in / Sign up

Export Citation Format

Share Document