Name
Title | ||
|---|---|---|
Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra |
Abstract | ||
|---|---|---|
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. |
Year | Venue | Keywords |
|---|---|---|
1978 | MVL '78 Proceedings of the eighth international symposium on Multiple-valued logic | additional programming,automated theorem-proving program,finite model,certain specified inference rule,known fact,ternary boolean algebra,unanswered question,new fact,invaluable aid,automated theorem-proving procedure,automated generation,mathematical model,automated theorem proving,boolean algebra,many valued logic,inference rule |
DocType | Citations | PageRank |
Conference | 12 | 5.79 |
References | Authors | |
2 | 2 | |