JPH06314200A - Proof construction support device - Google Patents

Abstract

(57) [Abstract] [Purpose] Regarding a proof construction support process by a computer, a proof construction support device which automatically generates a candidate of a template indicating the appearance position of a variable in an original logical formula and supports the designation of the logical formula. To aim. [Structure] The support processing unit 1 for applying a derivation rule to a logical expression is a template when an input logical expression is an expression in which a required term is substituted and an original logical expression is required as an application result of the derivation rule. The selection unit 2 is requested to process the logical expression returned by the template selection unit as the original logical expression, and the template selection unit 2 may select one or more values that can be the result of substitution of free variables of the logical expression. In the template determined by the input of the logical expression, the term is shown as the position of the free variable, a template having a combination of different free variable positions is generated, an input for selecting one of the generated templates is received, and the template is determined by the input of the logical expression. It is configured so that a logical expression in which the position of the term shown is a free variable is generated and returned to the support processing unit 1.

Description

Detailed Description of the Invention

[0001]

BACKGROUND OF THE INVENTION 1. Field of the Invention The present invention relates to a proof construction support device for supporting a user's proof construction work using a computer.

[0002]

2. Description of the Related Art An attempt is made to construct a proof that a user derives a formula of a conclusion from a formula of a premise by successively applying appropriate derivation rules. In such cases, it is considered that such proof construction work is supported by computer processing.

As is well known, the proof is one step of each proof by applying a derivation rule and the like to necessary formulas, proof fragments that are information of the proof process, and necessary axioms and theorems. Is advanced. Here, the derivation rule is, for example, an inference rule, a rewriting rule, a derivation rule, or the like.

The inference rule, which is applied to the whole equation and draws a conclusion from a premise, is shown in FIG. 2 (a). In the figure, B1, B2, etc. are predicate expressions, and C is a conclusion expression obtained by applying a certain inference rule to those presuppositions.

FIG. 2 (b) shows the format of the inference rule when each premise Bi is obtained based on the assumption Aij etc. (representing a set of assumptions enclosed in square brackets), and FIG. 2 (c) shows the rewriting rule. Shows the format of. “Applying” these derivation rules means that the expression specified by the user is parsed, and if it is a logical expression that satisfies the required condition, the precondition in the derivation rule or the expression before rewriting and the expression This is a process of performing pattern matching and, when the patterns match, drawing a conclusion or an expression after rewriting.

In such a proof construction support device, in order to apply the derivation rule specified by the above operation to obtain a result, and to facilitate the operation for the user to specify the derivation rule, Display all the derivation rules and let the user select from them, or display and select the applicable derivation rule candidates within the range of the formula, proof fragment, etc. entered by the user. Are supported by.

Here, the derivation rule of the inference rule ∃ shown in FIG. 2D is ∃x.P (x) (that is, if P (t / x) is proved,
It can be proved that there exists x with P (x) being true ”. However, P (t / x) is a logical expression in which the term t is substituted for the free variable x of the logical expression P (x).

Therefore, for example, a logical expression "0 = 0 + 0" is given, and when t is 0, an inference rule ∃ which is a derivation rule.
When the derivation rule of P is applied, first, P (0 / x) shows a general logical expression, so that matching is unconditionally obtained with 0 = 0 + 0.

Therefore, in order to express the conclusion in accordance with the derivation rule, it is necessary to know P (x), but the original logical expression (which is the original logical expression), which is 0 = 0 + 0 when substituted, is 0 = x + 0. It may be either x or x = x + x. Since various combinations of other variable appearance positions are possible, the conclusion cannot be determined.

Therefore, in order to continue the proof in such a case, the user must specify the original logical expression, and as the specifying method, for example, a method of counting the appearance positions of variables from the left, a logical expression A list of natural numbers in which each branch of the syntax tree is parsed by parsing, and the position on the syntax tree is represented by the number sequence of the branch that follows the root. There is a method of inputting the later logical expression and the original logical expression together.

However, in any of the above methods, the logical expression becomes complicated, the input becomes complicated, and the input error often occurs. An object of the present invention is to provide a proof construction support device that automatically generates a template candidate that indicates the appearance position of a variable in an original logical expression in the above case and assists in the specification of the logical expression.

[0012]

FIG. 1 is a block diagram showing the configuration of the present invention. The figure shows the configuration of the proof construction support device, which inputs a logical expression and a derivation rule, determines the application of the derivation rule to the logical expression, and, according to the applicable derivation rule, an application result corresponding to the logical expression. A proof construction support device having a support processing unit 1 for generating a template selection unit 2.

The support processing unit 1 discriminates that the input logical expression is an expression obtained by substituting a required term into a free variable of the original logical expression, and the original logical expression is required as an application result of the derivation rule. In this case, the input logical expression is passed to the template selecting unit 2 and the logical expression returned by the template selecting unit is processed as the original logical expression.

In the first invention, the template selection unit 2
Indicates a position that can be a result of substitution of free variables in the logical expression as the position of the free variable, generates a template having a combination of different free variable positions, and generates one template from the generated template. Receiving the input to select, the support processing unit 1 generates a logical expression in which the position indicated by the template defined by the input of the logical expression is a free variable.
Return to.

In the second invention, the template selection unit 2 indicates the template to be selected from a plurality of the templates according to a predetermined condition at the beginning of the selection, and inputs whether or not to select the template. receive.

[0016]

With the proof construction support device of the present invention, in the support processing such as proof construction, in order to apply the derivation rule to the logic expression in which the free variable is substituted, the original logical expression must be defined. The support device automatically generates a template indicating the position of the free variable of the original logical expression, displays it to the user, and causes the user to select one template.

Therefore, the user does not need to input the original logical expression itself or the input of the position of the free variable of the logical expression, and the user can easily and surely specify the necessary original logical expression. Can be done.

[0018]

FIG. 3 is a diagram showing an example of the processing flow of the proof construction support apparatus of the present invention. In the figure, for example, a logical expression designated by the user is input, and the user designates it. Alternatively, it shows a process when a derivation rule automatically selected by a support device is applied to the logical expression.

In FIG. 3, first, when the support processing unit 1 of FIG. 1 extracts a logical expression and a derivation rule in processing step 10, a syntax analysis is performed in processing step 11 and a syntax analysis result is identified in processing step 12, If the requirement as a logical expression is not satisfied, the derivation fails and the application process this time ends.

If the syntactic analysis is successful, processing step 13 performs pattern matching with the condition part of the derivation rule, and processing step 14 identifies whether or not the derivation rule is applicable based on the success or failure of the pattern match. This process ends as a derivation failure.

If the derivation rule is applicable, the support processing unit 1
In processing step 15, it is determined from the currently used derivation rule whether this logical expression is an expression with substitution and it is necessary to know the original logical expression in order to apply the derivation rule. If it is possible to proceed with the application of, the process proceeds to processing step 19 to perform the application processing.

When it is necessary to know the original logical expression, the support processing section 1 requests the template selecting section 2 for processing. Therefore, the template selection unit 2 creates a template based on the logical expression in processing step 16.

In the process of creating the template, the logical expression corresponding to P (t / x) is parsed, the position where the free variable x can appear syntactically is identified, and all the positions corresponding to the condition are identified. Replace zero or more positions with a predetermined placeholder symbol, and leave the positions that are not replaced with the substitution value t of 1
Create a template for all cases in which the replacement position for the placeholder symbol is different.

Therefore, for example, as in the above example, the logical expression 0
In the example of applying the derivation rule of the inference rule ∃ as the derivation rule to = 0 + 0, eight different templates are generated as shown in FIG. In the figure, "$$" is used as a placeholder symbol.

Next, the template selecting section 2 displays the template on the display device in the processing step 17, prompts the user to select, and waits for selection input. Therefore, the user selects a template by, for example, moving the cursor on the display screen to the display position of the desired template and pressing the designation key. Alternatively, each template is displayed with a number, and the user inputs the number of the template to be selected.

Further, according to the second invention, a template satisfying a certain condition, for example, a template in which the first free variable appearance position counted from the left of the expression is used as a placeholder,
Alternatively, a template or the like having all appearance positions as placeholders is first created and displayed as a so-called default.

On the other hand, the user indicates whether or not to adopt the default template by, for example, a predetermined one-key input, and the template selection unit 2 selects the other templates as described above only when the input is NO. Create and display in and let the user select.

By doing so, it becomes possible to further facilitate the user's designation of the template that is highly likely to be selected and to advance the processing quickly. When the user makes an input to select a template, the template selection unit 2 creates a logical expression in which the position indicated by the placeholder symbol of the selected template is a free variable and returns it to the support processing unit 1. Part 1 process step 19
Then, the process of applying the derivation rule with the logical expression as the original logical expression is performed.

As a result, when each template illustrated in FIG. 4 is designated, the derivation rule of the inference rule ∃ can be applied to generate the inference result shown on the right. The placeholder symbol used in the above description is always the one specified by the system, even if only the symbol specified by the system is used in advance, or the user can specify any symbol as the default. It may be specified.

Allowing the user to be designated in this manner is effective for avoiding confusion when a system-defined symbol already exists in a logical expression. Further, in the above description, when it is necessary to specify the original logical expression, a template candidate is always created and the user is allowed to select it. However, for example, the support processing unit 1 performs the processing step 15 in FIG.
When it is determined that the original logical expression is necessary in step 1, the user may be immediately asked whether or not to input the original logical expression.

Then, when the user inputs an original logical expression or inputs such as designating an appearance position of a free variable in the original logical expression, the support processing unit determines that the logical expression determined by the input is a derivation rule. It is checked whether or not it can be used as an original logical expression for application, and if it is a valid logical expression, the template selecting unit 2 is not requested to perform processing, and the processing is performed using that expression.

When an appropriate key input indicating that the inquiry is passed is made in response to the inquiry, the template selecting unit 2 is requested to perform the same processing as described above.
By doing this, in the case where a relatively simple logical expression is targeted, etc., rather than selecting a template, the user can directly specify the original logical expression and proceed with the work quickly. can do.

[0033]

As is apparent from the above description, according to the present invention, with respect to the support processing such as proof construction by a computer, when it is necessary to specify the original logical expression for the logical expression with substitution, the original logical expression Since a template candidate indicating the position where the variable appears in is automatically generated to support the specification of the logical expression, there is a remarkable industrial effect that work such as proof construction can be efficiently advanced.

[Brief description of drawings]

FIG. 1 is a block diagram showing the configuration of the present invention.

FIG. 2 is a diagram showing a format example of a derivation rule.

FIG. 3 is a flow chart of processing of the present invention.

FIG. 4 is a diagram illustrating a template example.

[Explanation of symbols]

 1 Support processing unit 2 Template selection unit 10 to 19 processing steps

Claims (2)

[Claims] 1. A support processing unit that inputs a logical expression and a derivation rule, determines whether the derivation rule is applied to the logical expression, and generates an application result corresponding to the logical expression according to the applicable derivation rule. A proof construction supporting device having (1), wherein a template selecting unit (2) is provided, and the supporting processing unit (1) substitutes a required term into a free variable of the input logical formula. Is an expression, and when it is determined that the original logical expression is required as the application result of the derivation rule, the input logical expression is passed to the template selection unit (2), and the logic returned by the template selection unit The expression is processed as the original logical expression, and the template selection unit (2) indicates the position that can be the substitution result of the free variable of the logical expression as the position of the free variable, and sets the combination of different free variable positions. Generate a template that has the generated template It is configured to receive an input for selecting one of the templates from the rate, generate a logical expression in which the position indicated by the template of the logical expression determined by the input is a free variable, and return the logical expression to the support processing unit (1). A proof construction support device characterized in that 2. The template selection unit (2) indicates the template to be selected from a plurality of the templates according to a predetermined condition at the beginning of the selection, and receives an input as to whether or not to select the template. The proof construction support device according to claim 1.