Finite Model Generation

In the recent years, a great portion of our effort has been spent on collaboration with mathematicians in the study of finite structures in discrete mathematics. We solved numerous open problems and make significant contributions in that field. This success shows the maturity of automated reasoning. These open problems also motivate us to look for new ideas and tools to attack them, thus making contributions to the field of automated reasoning.

Related Papers

  • Abel, R.J.R., Bennett, F.E., Zhang, H., Zhu, L.: (1997) Existence of HSOLSSOMs with types $h^n$ and $1^nu^1$, to appear in {\em J. of Combinatorial Designs}.
  • Abel, R.J.R., Bennett, F.E., Zhang, H.: (1997) Holey Steiner pentagon systems, {\em J. of Combinatorial Designs}.
  • Bennett, F.E., Zhang, H., Zhu, L.: (1997) Holey self-orthogonal Latin squares with symmetric orthogonal mates, to apper in {\em Annuals of Combinatorics}.
  • Bennett, F.E, Wei, R., Zhang, H.: (1997) Holey Schroder designs of type $2^nu^1$, to appear in {\em J. of Combinatorial Designs}.
  • Bennett, F.E, Zhang, H.: (1997) Existence of $(3,1,2)$--HCOLS and $(3,1,2)$--HCOLS, to appear in {\em J. of Combina. Math. and Combina. Computing}.
  • Bennett, F.E., Chang, Y., Yin, J., Zhang, H.: (1997) Existence of HPMDs with block size five, to appear in {\em J. of Combinatorial Designs}.
  • Abel, R.J.R., and Zhang, H.: (1997) Direct constructions for certain types of HMOLS, to appear in {\em J. of Discrete Mathematics}.
  • Bennett, F.E., Du, B., Zhang, H.: (1997) Existence of self-conjugate self-orthogonal diagonal Latin squares, to appear in {\em J. of Combinatorial Designs}.
  • Zhang, H.: (1997) Specifying Latin squares in propositional logic, in R. Veroff (ed.): Automated Reasoning and Its Applications, Essays in honor of Larry Wos, Chapter 6, MIT Press.
  • Bennett, F.E, Wei, R., Zhang, H.: (1997) HPMDs of type $2^n3^1$ with block size four and related HCOLS, {\em J. of Combina. Math. and Combina. Computing}, 23, 33-45
  • Abel, R.J.R., Colborn, C.J., Yin, J., Zhang, H.: (1997) Existence of incomplete transversal designs with block size five and any index, {\em Designs, Codes and Cryptography}, 10, 275-307
  • Bennett, F.E., Wei, R., Zhang, H.: HPMDs of type $2^n3^1$ with block size four and related HCOLS, {\em J. of Combin. Math. and Combin. Comp.} {\bf 23} (1997) 33-45.
  • Zhang, H., Bennett, F.E.: Existence of some $(3,2,1)$--HCOLS and $(3,2,1)$--HCOLS. {\em J. of Combinatoric Mathematics and Combinatoric Computing}, 22 (1996) 13-22.
  • Bennett, F.E., Zhang, H., Zhu, L.: (1996) Self-orthogonal Mendelsohn triple systems. {\em Journal of Combinatoric Theory} {\bf A} 73 (1996), 207-218.

    Some of these papers can be found here.


    Hantao Zhang
    Updated