| 摘要 |
PROBLEM TO BE SOLVED: To provide a device for efficiently proving theorem while updating and holding a useful theorem for 1st-order predicate closed logic. SOLUTION: An input part 1' inputs a 1st-order predicate closed formulaϕ, the number (m) of times of dual lead-out in one lead-out/selection operation, the number (n) of times of simplification, the number (p) of nodes, the number (r) of times of operations and parametersα,βandγfor determining adaptation, etc. A conversion part 2 converts the expressionϕto an indexed node set S and a calculation part 3 calculates the complexing d(C) of the structure of a node form C. A load-out part in a theorem generation part 4 executes indexed dual lead-out/simplification to the node of SUDS with a free set as a DS and delivers the generated indexed node set to a selection part 42 as a new DS. The selection part 42 calculates the adaptation of the respective nodes of the DS by utilizing a complication calculation part 3 and attains the new DS. A control part 43 outputs the DS to an output part 5 when the lead-out/selection operation is repeated for (r) times.
|
