Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra

摘要

The thrust of this paper is: first, to answer certain previously unanswered questions in the field of Ternary Boolean algebra; second, to describe the method, utilizing an automated theorem-proving program as an invaluable aid, by which these answers were obtained; and third, to informally give the characteristics of those problems to which the method can be successfully applied. The approach under study begins with known facts in the form of axioms and lemmas of the field being investigated, finds by means of certain specified inference rules new facts, and continues to reason from the expanding set of facts until the problem at hand is solved or the procedure is interrupted. The solution often takes the form of a finite model or of a counterexample to the underlying conjecture. The model and/or counterexample is generated with the aid of an already existing automated theorem-proving procedure and without any recourse to any additional programming.