Interferons and Schemas: Control Techniques for Automated Reasoning and Generalized Search

摘要

A new technique, interferon weighting for controlling the automated search for proofs of theorems in the first order logic is proposed. The technique is based on the Wos' resonance strategy and the schema theorem from the theory of genetic algorithms. Interferon weighting, in turn, suggests a form for a generalized search technique — one that is a variant of the standard genetic algorithm. Preliminary experimental results supporting the use of interferons as a control strategy are reported. The experiments documented in this paper were conducted on a customized version of the open-source proof engine OTTER 3.0 (Organized Techniques for Theorem-proving and Effective Reasoning) developed by McCune at Argonne National Laboratories.