Extending Finite Model Searching with Congruence Closure Computation - Artificial Intelligence and Symbolic Computation - page 102

References
1. P.J. Downey, R. Sethi and R.E. Tarjan, Variations on the common subexpression
problem, J. ACM 27(4): 758-771, 1980.
2. M. Fujita, J. Slaney and F. Bennett, Automatic generation of some results in finite
algebra, Proc. 13th IJCAI , 52-57, 1993.
3. R. Hasegawa, M. Koshimura and H. Fujita, MGTP: A parallel theorem prover
based on lazy model generation, Proc. CADE-11 , LNAI 607, 776-780, 1992.
4. S. Kim and H. Zhang, ModGen: Theorem proving by model generation, Proc. 12th
AAAI , 162-167, 1994.
5. V. Kumar, Algorithms for constraint satisfaction problems: A survey, AI Magazine
13(1): 32-44, 1992.
6. R. Manthey and F. Bry, SATCHMO: A theorem prover implemented in Prolog,
Proc. CADE-9 , LNCS 310, 415-434, 1988.
7. W. McCune, A Davis-Putnam program and its application to finite first-order
model search: Quasigroup existence problems. Technical Report ANL/MCS-TM-
194, Argonne National Laboratory, 1994.
8. G. Nelson and D.C. Oppen, Fast decision procedures based on congruence closure,
J. ACM 27(2): 356-364, 1980.
9. R. Nieuwenhuis and A. Oliveras, Congruence closure with integer offsets, Proc.
10th LPAR , LNAI 2850, 78-90, 2003.
10. J. Slaney, FINDER: Finite domain enumerator - system description, Proc. CADE-
12 , LNCS 814, 798-801, 1994.
11. J. Slaney, M. Fujita and M. Stickel, Automated reasoning and exhaustive search:
Quasigroup existence problems, Computers and Mathematics with Applications
29(2): 115-132, 1995.
12. G. Sutcliffe and C. Suttner, The TPTP problem library for automated theorem
proving. http://www.cs.miami.edu/~tptp/
13. J. Zhang, Problems on the generation of finite models, Proc. CADE-12 , LNCS 814,
753-757, 1994.
14. J. Zhang, Constructing finite algebras with FALCON, J. Automated Reasoning
17(1): 1-22, 1996.
15. J. Zhang and H. Zhang, Constraint propagation in model generation, Proc. Int'l
Conf. on Principles and Practice of Constraint Programming , LNCS 976, 398-414,
1995.
16. J. Zhang and H. Zhang, SEM: A system for enumerating models, Proc. 14th IJCAI ,
298-303, 1995.