Publications

Journal Papers and Book Chapters

• F.B. Bennett, B. Du, H. Zhang: Conjugate orthogonal diagonal latin squares with missing subsquares, Wal Wallis (ed.) Designs 2002: Further Computational and Constructive Design Theory, Ch 2, Kluwer Academic Publishers, Boston, 2003.
• Zhu, L., Zhang, H.: Completing the spectrum of r-orthogonal latin squares. Discrete Mathematics 258 (2003)
• P. Baumgartner, H. Zhang, First-order theorem proving, special issue, Journal of Symbolic Computation, 36, 2003.
• Bennett, F.E., Du, Beiliang, Zhang, H.: Existence of self-orthogonal diagonal Latin squares with a missing subsquare, Discrete Mathematics, 261 (2003) 69-86
• Q. Han, Y. Ye, H. Zhang, J. Zhang: On approximation of Max-Vertex-Cover, European Journal of Operations Research, 143:2 (2002) 342-355
• Bennett, F.E., Ge, G., Zhang, H., Zhu, L.: Holey Steiner pentagon systems and related designs, Journal of Statistical Planning and Inference, 106 (2002) 353-373
• Xu, Y., Zhang, H., Zhu, L.: Existence of frame SOLS of type $a^nb^1$, Discrete Mathematics, 250 (2002) 211-230
• Zhu, L., Zhang, H.: A few more r-orthogonal Latin squares. Discrete Mathematics 238 (2001) 183-191
• Bennett, F.E., Du, B., Zhang, H.: Existence of (3,1,2)-conjugate orthogonal diagonal latin squares. J. of Combinatorial Designs 9: 297-308, 2001
• Abel, J., Bennett, F.E., Zhang, H., Zhu, L.: Steiner pentagon covering designs. Discrete Mathematics, 231 (2001) 11-26
• Bennett, F.E., Kang, Q., Lei, J., Zhang, H.: Large sets of disjoint pure Mendelsohn triple systems. J. of Statistical Planning and Inference 95 (2001) 89-115
• Abel, J., Bennett, F.E., Zhang, H., Zhu, L.: A few more incomplete self-orthogonal Latin squares and related designs. Australasian J. of Combinatorics, 21 (2000) 85-94.
• Abel, R.J.R., Bennett, F.E., Zhang, H., Zhu, L.: Existence of HSOLSSOMs with types $h^n$ and $1^nu^1$, Ars Combinatoria 55 (2000) 97-115.
• Abel, J., Bennett, F.E., Zhang, H.: Perfect Mendelsohn designs with block size six. J. of Statistical planning and inference, 86 (2000) 287-319
• Zhang, H., Stickel, M.: Implementing the Davis-Putnam method, J. of Automated Reasoning 24: 277-296, 2000.
• Abel, R.J.R., Bennett, F.E., Zhang, H.: Holey Steiner pentagon systems, J. of Combinatorial Designs 7 (1999) 41-56
• Bennett, F.E, Zhang, H.: (1998) Existence of (3,1,2)-HCOLS and (3,1,2)-HCOLS, J. of Combinatoric Mathematics and Combinatoric Computing, 27 (1998) 53-64
• Bennett, F.E., Yin, J., Zhang, H., Abel, R.J.R.: Perfect Mendelsohn packing designs with block size five, J. of Designs, Codes and Cryptography, 14, 5-22 (1998).
• Bennett, F.E, Wei, R., Zhang, H.: Holey Schroder designs of type $2^nu^1$, J. of Combinatorial Designs, 6 131-150, 1998
• Bennett, F.E., Du, B., Zhang, H.: Existence of self-conjugate self-orthogonal diagonal Latin squares, J. of Combinatorial Designs, 6 51-62, 1998.
• Abel, R.J.R., and Zhang, H.: Direct constructions for certain types of HMOLS, J. of Discrete Mathematics, 181 (1998) 1-17
• Bennett, F.E., Du, B., Zhang, H.: (1997) Existence of conjugate orthogonal diagonal Latin squares, J. of Combinatorial Designs, 5: 449-461.
• 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., Zhang, H., Zhu, L.: Holey self-orthogonal Latin squares with symmetric orthogonal mates, Annuals of Combinatorics, Vol. 1, No. 2 (1997) 107-118
• Bennett, F.E., Chang, Y., Yin, J., Zhang, H., Existence of HPMDs with block size five, J. Combin. Designs, 5 (1997), 257-273.
• Abel, R.J.R., Colborn, C.J., Yin, J., Zhang, H.: Existence of incomplete transversal designs with block size five and any index, Designs, Codes and Cryptography, 10, 275-307 (1997)
• Bennett, F.E., Wei, R., Zhang, H.: HPMDs of type $2^n3^1$ with block size four and related HCOLS, J. of Combinatoric Mathematics and Combinatoric Computing, 23 (1997) 33-45.
• Zhang, H. (ed.): Automated Mathematical Induction, April 1996, Kluwer Academic Publishers.
• Zhang, H., Bonacina, M.P., Hsiang, H.: PSATO: a distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation (1996) 21, 543-560.
• Zhang, H., Bennett, F.E.: Existence of some (3,2,1)-HCOLS and (3,2,1)-HCOLS. J. of Combinatoric Mathematics and Combinatoric Computing, 22 (1996) 13-22.
• Bennett, F.E., Zhang, H., Zhu, L.: (1996) Self-orthogonal Mendelsohn triple systems. Journal of Combinatoric Theory A 73 (1996), 207-218.
• Kapur, D., Zhang, H.: (1995) An overview of Rewrite Rule Laboratory. J. of Computer and Mathematics with Applications, 29, 2, 91-114.
• Zhang, H.: Contextual rewriting for theorem proving. Journal of Fundamenta Informaticae, (1995) 24:107-123
• Kapur, D., Sivakumar, G., Zhang, H.: (1995) Proving termination of AC-rewrite Systems. J. of Automated Reasoning, 14:293-316.
• Zhang, H.: (1994) A new strategy for the boolean ring based approach to first order theorem proving. J. of Symbolic Computation, 17, 189-211.
• Zhang H.: (1993) Automated proofs of equality problems in Overbeek's competition. J. of Automated Reasoning, 11: 333-351, 1993.
• Zhang, H., Hua, G.X.: (1993) Proving Ramsey theorem by the cover set induction: a case and comparison study. The Annals of Mathematics and Artificial Intelligence, Volume 8, 383-405.
• Kapur, D., Narendran, P., Zhang, H.: (1991) Automating inductionless induction by test sets. J. of Symbolic Computation, 11, 83-111.
• Kapur, D., Narendran, P., Rosenkrantz, D., Zhang, H.: (1991) Sufficient completeness, ground reducibility and their complexity. Acta Informatica 28, 311-350.
• Kapur, D., Zhang, H.: (1991) A case study of the completion procedure: Proving ring commutativity problems. In J.-L. Lassez and G. Plotkin (eds.): Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, MA.
• Zhang, H.: (1990) Automated proof of ring commutativity problems by algebraic methods. J. of Symbolic Computation 9, 423-427.
• Zhang, H., Kapur, D.: (1990) Unnecessary inferences in associative-commutative completion procedures. Mathematical System Theory 23, 175-206.
• Burckert, H.-J., Herold, A., Kapur, D., Siekmann, J.H., Stickel, M., Tepp, M., Zhang, H. (1988) Opening the AC-unification race. J. of Automated Reasoning, (4), 465-474.
• Kapur D., Zhang, H.: (1988) Proving equivalence of different axiomatizations of free groups. J. of Automated Reasoning (4) 331-352.
• Kapur, D., Narendran, P., Zhang, H.: (1987) On sufficient-completeness and related properties of term rewriting systems. Acta Informatica Vol. 24, 395-415.

Refereed Conference Papers

• Shen, H., Zhang, H..: Improving Exact Algorithms for MAX-2-SAT, Eighth International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, January 2004.
• Zhang, H., Manya, F., Shen, H.: Exact algorithsm for MAX-SAT, Proc. of International Workshop on First Order Theorem Proving, 2003.
• Shen, H., Zhang, H..: An empirical study of MAX-2-SAT phase transitions. Proc. of LICS Workshop on Phase Transitions, Ottawa, Canada, July 2003.
• Zhang, H.: (2003) Efficient data structure for clauses in SAT solvers, Proc. of Intl. Workshop on Microprocessor Testing and Verification, Austin, TX.
• Zhang, H.: (2002) Generating college conference basketball schedules by a SAT solver, Proc. of Fifth International Symposium on Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, 2002, pp. 281-291.
• Zhang, H.: (2002) A random jump strategy for combinatorial search. Proc. of Sixth International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, FL, 2002.
• Zhang, H.: (2000) Lemma generation in the Davis-Putnam procedure. Proc. of Workshop on Automated Model Building, International Conference on Automated Deduction (CADE-2000).
• Hubbard, D., Zhang, H.: (1999) A case study of automated test cases generation for LDP. Proc. of Lucent Conference on Automated Software Testing (AST'99) pp. 141-150, Murray Hill, NJ.
• Zhang, H.: (1998) Automated generation of test cases using Testmaster. Proc. of Lucent Conference on Automated Software Testing (AST'98) pp. 23-32, Chicago, IL.
• Zhang, H.: (1997) SATO: An efficient propositional prover, Proc. of International Conference on Automated Deduction (CADE-97). pp. 308-312, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.
• Zhang, J., Zhang, H.: (1996) Combining local search and backtracking techniques for constraint satisfaction, in Proc. of National Conference on Artificial Intelligence (AAAI-96), Vol 1, pp. 369-374, AAAI Press/MIT Press.
• Zhang, J., Zhang, H.: (1996) Generating models by SEM, in Proc. of International Conference on Automated Deduction (CADE-96), pp. 308-312, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag.
• Zhang, H., Stickel, M.: (1996) An efficient algorithm for unit propagation. In Kautz and Selman (eds.) Proc. of the Fourth International Symposium on Artificial Intelligence and Mathematics. Ft. Lauderdale, Florida, pp. 166-179.
• Zhang, J., Zhang, H.: (1995) Constraint propagation in model generation. In Ugo Montanari (ed:) Proc. of 1st International Conference on Principles and Practice of Constraint Programming (CP95) Marseille, September 19-22, 1995.
• Zhang, J., Zhang, H.: (1995) SEM: a System for Enumerating Models. Proc. of International Joint Conference on Artificial Intelligence (IJCAI95) Montreal, August 11-18, 1995, pp. 298-303.
• Stickel, M., Zhang, H: (1995) Studying quasigroup identities by rewriting techniques: problems and first results. In Hsiang, J. (ed,): Proc. of International Conference on Rewrite Techniques and Applications (RTA-95) Lecture Notes in Computer Science, Springer-Verlag, pp. 450-456.
• Zhang, H., Hsiang, J.: (1994) Solving open quasigroup problems by propositional reasoning. Proc. of International Computer Symposium, Hsinchu, Taiwan.
• Zhang, H., Bonacina, M. P.: (1994) Cumulating search in a distributed computing environment: A case study in parallel satisfiability. Proc. of the First International Symposium on Parallel Symbolic Computation (PASCO-94), Linz, Austria, September 1994.
• Kim, S., Zhang, H.: (1994) ModGen: Theorem proving by model generation. Proc. of National Conference of American Association on Artificial Intelligence (AAAI-94), Seattle, WA. MIT Press, pp. 162-167.
• Kapur, D., Zhang, H.: (1994) Automated induction: explicit vs. implicit. In Proc. of Third International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida.
• Hua, G.X., Zhang, H.: (1993) Formal verification of circuit designs in VHDL. In Proc. of 9th International Conference on Advanced Science and Technology, Motorola, Inc., Schaumburg, Illinois.
• Zhang, H.: (1993) A case study of completion modulo distributivity and Abelian groups. In Kirchner, C. (ed,): Proc. of International Conference on Rewrite Techniques and Applications (RTA-93), Montreal, Canada. Lecture Notes in Computer Science, V. 690, Springer-Verlag. pp. 32-46.
• Lee, S.K., Lin, X., Zhang, H.: (1992) Efficient decision procedures for strength logic. In Proc. of 1992 Pacific-Rim International Conference on Artificial Intelligence. South Korea.
• Zhang, H.: (1992) Proving group isomorphism theorems: a case study of conditional completion. In J.L. Remy and M. Rusinowitch (eds.): Proc. of 3rd International Workshop on Conditional Term Rewriting Systems. Pont-A-Mousson, France. Lecture Notes in Computer Science, V. 656, Springer-Verlag. pp. 302-306.
• Zhang, H.: (1992) Implementing contextual rewriting. In J.L. Remy and M. Rusinowitch (eds.): Proc. of 3rd International Workshop on Conditional Term Rewriting Systems. Pont-A-Mousson, France. Lecture Notes in Computer Science, V. 656, Springer-Verlag. pp. 363-377.
• Zhang, H.: (1992) Herky: High-performance rewriting techniques in RRL. In Kapur, D.: (ed.): Proc. of 1992 International Conference of Automated Deduction. Saratoga, NY. Lecture Notes in Artificial Intelligence, 607, Springer-Verlag. pp. 696-700.
• Hua, G.X., Zhang, H.: (1992) FRI: Failure Resistant Induction in RRL. In Kapur, D.: (ed.): Proc. of 1992 International Conference of Automated Deduction. Saratoga, NY. Lecture Notes in Artificial Intelligence, 607, Springer-Verlag. pp. 691-695.
• Zhang, H., Hua, G.X.: (1992) Proving the Chinese remainder theorem by the cover ste induction. In Kapur, D.: (ed.): Proc. of 1992 International Conference of Automated Deduction. Saratoga, NY. Lecture Notes in Artificial Intelligence, 607, Springer-Verlag. pp. 431-445.
• Zhang, H.: (1992) A new strategy for the boolean ring based approach to first order theorem proving. In Proc. of Second International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida.
• Zhang, H., Hua, G.X.: (1992) Proving Ramsey theorem by the cover set induction: a case and comparison study. In Proc. of Second International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida.
• Hua, G.X., Zhang, H.: (1992) Axiomatic semantics of a hardware specification language. In Proc. of the Second IEEE Great Lakes Symposium on VLSI Design. Kalamazoo, MI. pp. 183-190.
• Zhang, H.: (1990) Approximate reasoning in strength logic. Proc. of The IEEE 20th International Symposium on Multiple-Valued Logic, Charlotte, North Carolina, IEEE Computer Society Press, 262-269.
• Kapur, D., Sivakumar, G., Zhang, H.: (1990) A new method for proving termination of AC-rewrite Systems. Proc. of 10th Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, India.
• Zhang, H.: (1989) Constructor model as abstract data types. In Rus, T. (ed.) Proc. of First International Conference on Algebraic Methodology and Software Technology, Iowa City, Iowa.
• Kapur, D., Zhang, H.: (1989) An overview of RRL: Rewrite Rule Laboratory. Proc. of the third International Conference on Rewriting Techniques and its Applications (RTA-89), April 1989, Chapel Hill, NC, Lecture Notes in Computer Science, Vol. 355, Springer-Verlag, Berlin, 513-529.
• Zhang, H., Kapur, D.: (1989) Consider only general superpositions in completion procedures. Proc. Third International Conference on Rewriting Techniques and its Applications (RTA-89), April 1989, Chapel Hill, NC, Lecture Notes in Computer Science, Vol. 355, Springer-Verlag, Berlin, 513-529.
• Kapur, D., Zhang, H.: (1988) RRL: a Rewrite Rule Laboratory. In Lusk, R. and Overbeek, R. (eds.) Proc. of the 9th International Conference on Automated Deduction (CADE-9), Argonne, Illinois. Lecture Notes in Computer Science, Vol. 310, Springer-Verlag, Berlin, 768-769.
• Zhang, H., Kapur, D., Krishnamoorthy, M.S.: (1988) A mechanizable induction principle for equational specifications. In Lusk, R. and Overbeek, R. (eds.) Proc. of the 9th International Conference on Automated Deduction (CADE-9), Argonne, Illinois. Lecture Notes in Computer Science, Vol. 310, Springer-Verlag, Berlin, 250-265.
• Zhang, H., Kapur, D.: (1988) First-order logic theorem proving using conditional rewrite rules. In Lusk, R. and Overbeek, R. (eds.) Proc. of the 9th International Conference on Automated Deduction (CADE-9), Argonne, Illinois. Lecture Notes in Computer Science, Vol. 310, Springer-Verlag, Berlin, 1-20.
• Kapur, D., Narendran, P., Zhang, H.: (1986) Complexity of sufficient-completeness. Proc. of 6th Conference on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India. Lecture Notes in Computer Science, Vol. 241, Springer-Verlag, Berlin, 426-442.
• Kapur, D., Sivakumar, G., Zhang, H.: (1986) RRL: a Rewrite Rule Laboratory. Proc. of the 8th International Conference on Automated Deduction (CADE-8), Oxford, England, Lecture Notes in Computer Science, Vol. 230, Springer-Verlag, Berlin, 692-693.
• Kapur, D., Narendran, P., Zhang, H.: (1986) Proof by induction using test sets. Proc. of Eighth International Conference on Automated Deduction (CADE-8), Oxford, England, Lecture Notes in Computer Science, Vol. 230, Springer-Verlag, Berlin, 99-117.
• Kounalis, E., Zhang, H.: (1985) A general completeness test for equational specifications. Proc. of Hungarian Conference of Computer Science.
• Zhang, H., Remy, J.L.: (1985) Contextual rewriting. Proc. of rewriting techniques and application, Dijon, France. Lecture Notes in Computer Science, Vol. 202, Springer-Verlag, Berlin, 201-220.
• Zhang, H., Lescanne, P.: (1984) Path of symbols ordering. Proc. of 6th European Conference on Artificial Intelligence, Pisa, Italy. In T. O'Shea (ed.): Advances in Artificial Intelligence, Elsevier Science Publishers B.V. North-Holland.
• Remy, J.L., Zhang, H.: (1984) Reveur4: a system for validating conditional specifications of abstract data types. Proc. 6th European Conference on A.I. Pisa, Italy. In T. O'Shea (ed.): Advances in Artificial Intelligence, Elsevier Science Publishers B.V. North-Holland.