Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Publications

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.

Hantao Zhang