Conclusion in logical models. Inference rule method

Two methods are most commonly used. The first is the rule of inference method, or the method of natural (natural) inference, so named because the type of reasoning used in the predicate calculus approaches that of ordinary human reasoning. The second is the resolution method. It is based on the calculus of resolvents.

This article discusses the inference rule method . In predicate logic, the rule is used, which of the two expressions and displays a new expression .

Different literature contains different names for the method of inference rules, for example, deductive inference rules or, more often, modus ponens . The principle of operation of inference rules is well illustrated by the following example:

In predicate logic, there are universal rules that operate on formulas containing free variables. Solving problems (drawing conclusions) in logical models can be based on the application of similar rules to the original set of true predicates as evidence of the correctness of a composite predicate. Such a method of obtaining a solution is called non-axiomatic or in other words - natural, natural and coincides with the output methods in production models.

Since the answer is obtained as a conclusion from a combination of already existing logical formulas, by analogy with the conclusions in production models it can be called a direct (inverse) conclusion. However, it should always be borne in mind that in formal logic, cause-effect relationships are ignored.

The essence of the inference procedure is the recursive use of the substitution of known values ​​in a composite predicate. In this case, it is guaranteed in principle that the proof of the truth of the result can be verified by a formal procedure.

If, in a formal logical model, the mechanism of logical inference uses the method of inference rules, that is, the basis of this model is attributed to productional or logical-linguistic.

Example: solution output in a logical model based on an inference rule - modus ponens.

Statements are given:

Required to prove the statement "Socrates is mortal . "

Decision:

Step 1. Imagine the statements in predicate form:

Step 2. Based on the inference rule (modus ponens) and the substitution (Socrates / X) in the first predicate, we get the statement:

  "Socrates is a living thing." 

Step 3. Based on the inference rule (modus ponens) and the substitution (Socrates / Y) in the third predicate, we obtain the statement:

  "Socrates is mortal"