Abstract
An automated first-order theorem prover, armed with appropriate strategies, will find a proof of a true conjecture, but will, in theory, run indefinitely if no proof exists. In reality, if no proof exists, the execution will be terminated by user-defined constraints, such as running time or memory usage limit. In this case the the question of validity of the conjecture remains unanswered. An automated first-order model generator gives one the ability to find counterexamples, if any exist, showing that the conjecture is invalid. A model generator also helps find the illustrations of previously proved theorems. It can be viewed as a natural extension of a theorem prover.
An automated finite first-order model generator has been developed. The problem is viewed as a first-order satisfiability problem. Most existing model generators convert the problem from first-order to propositional satisfiability by converting the input first-order clauses into propositional clauses. This generator, unlike others, stores the input first-order clauses and solves the problem directly. It uses an exhaustive backtracking algorithm with weight-based splitting. A negative constraint propagation i's one of the features of this generator. The tests showed that this model generator performs on par with others on small problems. On larger problems, the backtracking nature of the algorithms slows the search down significantly. On several problems, this model generator outperforms SEM, another program that uses the direct approach to solving first-order satisfiability problem.
Recommended Citation
Shumsky, Olga; Ercal, Fikret; and Wilkerson, Ralph W., "New Methods in Finite First-Order Model Search" (1996). Computer Science Technical Reports. 189.
https://scholarsmine.mst.edu/comsci_techreports/189
Department(s)
Computer Science
Report Number
CSc-96-01
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1996 University of Missouri - Rolla, All rights reserved
Publication Date
1996-05-01
Comments
The first Author is a Graduate Student
This report is substantially the text of the M.S. thesis of the first author, completed May 1996.
Acknowledgements:
I would like to thank Drs. Wilkerson, Ercal and Morgan for serving on my thesis committee and for their advice on this project. I would like to extend my gratitude to the faculty and staff of the Computer Science Department at the University of Missouri-Rolla for their knowledge, patience, support and guidance over the last five years. It has made a tremendous difference in my life.
My sincere thanks go to the people at Argonne National Laboratory, especially to Larry Wos and William McCune, for the opportunity to participate in the summer research program there. I thank William McCune for sharing his time, energy and expertise in the beginning of this project and thus making it possible. Working under his guidance has been an enlightening experience.
Finally, I thank my parents for their unyielding support and love, sacrifice, and understanding.