Problem corner: Non-Horn problems (Q1819949)

The goal of automated reasoning research is to discover ways to solve problems. Specific problems have always been the spur to research in the field, and solving them the reward for inventing and implementing new ideas. Therefore it will be appropriate, hopefully useful, and certainly enjoyable if this Journal provides a regular forum for the presentation and discussion of specific problems in some detail. This column will be hosted by the ''Argonne group'' and the ''Kaiserslautern group'', who will start the ball rolling by presenting here several sets of problems over the next several issues. Our intention is to present in each issue a set of problems that illuminate some area of automated reasoning. We will give rigorous formulations of the problems, their complete solutions where possible, and some discussion of the interesting features of each problem or its solution. We certainly encourage others to submit problem sets, comment on the problems or solutions presented here, and in general participate in this column.