About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Paper
A note on syntactic symmetry and the manipulation of formal systems by machine
Abstract
In the past few years, digital computer programs that depart from the traditional numerical computation and data processing for which these machines were conceived have become increasingly commonplace. In many of these programs, the computer is called upon to manipulate a complex formal logistic system as a tool to implement the solution of a problem. This paper is concerned with the problem of efficient machine manipulation of formal systems in which the predicates display a high degree of symmetry. The solution to the problem, embodied in a theorem and a rule of syntactic symmetry is specified in Section I. The theorem is in fact a metatheorem concerning formal systems, and is used in the synthesis of proofs. On the other hand, the rule is an invaluable aid in the search for a proof by the so-called analytic method. In Section II, the set of all syntactic symmetries for a given set of formulas is constructed and displayed in a form conducive to minimum effort programming for a computer. © 1959 Academic Press Inc.
Related
Conference paper
A fortran-compiled list-processing language
Conference paper