{'fraction_non_alphanumeric': 0.006016847172081829, 'fraction_numerical': 0.0, 'mean_word_length': 5.449612403100775, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Some Experiments on the Applicability of Folding Architecture Networks to Guide Theorem Proving

One of the major problems in theorem proving is control of the proof search. A promising approach is the application of machine learning techniques for the acquisition of search control knowledge by learning from successful proof searches. In this paper we brieey discuss this idea and existing machine learning techniques for this task. We suggest neural folding architecture networks together with supervised training algorithms as a very promising candidate for learning search control knowledge. This suggestion is based on two sets of experiments in which we applied folding architecture networks to term ordering problems and clause classiication tasks resulting from the proof search of the equational theorem prover DISCOUNT .