REVEUR 4: A System for Validating Conditional Algebraic Specifications of Abstract Data Types. - Jean-Luc Rémy; Hantao Zhang 001 (ECAI, 1984)

Contextual Rewriting. - Hantao Zhang 001; Jean-Luc Rémy (RTA, 1985)

Proof by Induction Using Test Sets. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (CADE, 1986)

RRL: A Rewrite Rule Laboratory. - Deepak Kapur; G. Sivakumar; Hantao Zhang 001 (CADE, 1986)

Complexity of Sufficient-Completeness. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (FSTTCS, 1986)

On Sufficient-Completeness and Related Properties of Term Rewriting Systems. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (Acta Informatica, 1987)

RRL: A Rewrite Rule Laboratory. - Deepak Kapur; Hantao Zhang 001 (CADE, 1988)

First-Order Theorem Proving Using Conditional Rewrite Rules. - Hantao Zhang 001; Deepak Kapur (CADE, 1988)

A Mechanizable Induction Principle for Equational Specifications. - Hantao Zhang 001; Deepak Kapur; Mukkai S. Krishnamoorthy (CADE, 1988)

Opening the AC-Unification Race. - Hans-Jürgen Bürckert; Alexander Herold; Deepak Kapur; Jörg H. Siekmann; Mark E. Stickel; Michael Tepp; Hantao Zhang 001 (J. Autom. Reason., 1988)

Proving Equivalence of Different Axiomatizations of Free Groups. - Deepak Kapur; Hantao Zhang 001 (J. Autom. Reason., 1988)

An Overview of Rewrite Rule Laboratory (RRL). - Deepak Kapur; Hantao Zhang 001 (RTA, 1989)

Consider Only General Superpositions in Completion Procedures. - Hantao Zhang 001; Deepak Kapur (RTA, 1989)

A New Method for Proving Termination of AC-Rewrite Systems. - Deepak Kapur; G. Sivakumar; Hantao Zhang 001 (FSTTCS, 1990)

Approximate Reasoning in Strength Logic. - Hantao Zhang 001 (ISMVL, 1990)

Automated Proof of Ring Commutativity Problems by Algebraic Methods. - Hantao Zhang 001 (J. Symb. Comput., 1990)

Unnecessary Inferences in Associative-Commutative Completion Procedures. - Hantao Zhang 001; Deepak Kapur (Math. Syst. Theory, 1990)

Using Algebraic Specification in Floyd-Hoare Assertions. - Hantao Zhang 001; Angshuman Guha; Xin Hua (AMAST, 1991)

A Case Study of the Completion Procedure: Proving Ring Commutativity Problems. - Deepak Kapur; Hantao Zhang 001 (Computational Logic - Essays in Honor of Alan Robinson, 1991)

Sufficient-Completeness, Ground-Reducibility and their Complexity. - Deepak Kapur; Paliath Narendran; Daniel J. Rosenkrantz; Hantao Zhang 001 (Acta Informatica, 1991)

Automating Inductionless Induction Using Test Sets. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (J. Symb. Comput., 1991)

FRI: Failure-Resistant Induction in RRL. - Xin Hua; Hantao Zhang 001 (CADE, 1992)

Herky: High Performance Rewriting in RRL. - Hantao Zhang 001 (CADE, 1992)

Proving the Chinese Remainder Theorem by the Cover Set Induction. - Hantao Zhang 001; Xin Hua (CADE, 1992)

Proving Group Isomorphism Theorems (Extended Abstract). - Hantao Zhang 001 (CTRS, 1992)

Implementing Contextual Rewriting. - Hantao Zhang 001 (CTRS, 1992)

Axiomatic semantics of a hardware specification language. - Xin Hua; Hantao Zhang 001 (Great Lakes Symposium on VLSI, 1992)

Formal Semantics of VHDL for Verification of Circuit Designs. - Xin Hua; Hantao Zhang 001 (ICCD, 1993)

A Case Study of Completion Modulo Distributivity and Abelian Groups. - Hantao Zhang 001 (RTA, 1993)

Proving Ramsey's Theorem by the Cover Set Induction: A Case and Comparison Study. - Hantao Zhang 001; Gary Xin Hua (Ann. Math. Artif. Intell., 1993)

Automated Proofs of Equality Problems in Overbeek's Competition. - Hantao Zhang 001 (J. Autom. Reason., 1993)

ModGen: Theorem Proving by Model Generation. - Sun Kim; Hantao Zhang 001 (AAAI, 1994)

Cumulating Search in a Distributed Computing Environment: A Case Study in Parallel Satisfiability. - Hantao Zhang 001; Maria Paola Bonacina (PASCO, 1994)

A New Method for the Boolean Ring Based Theorem Proving. - Hantao Zhang 001 (J. Symb. Comput., 1994)

Constraint Propagation in Model Generation. - Jian Zhang 001; Hantao Zhang 001 (CP, 1995)

SEM: a System for Enumerating Models. - Jian Zhang 001; Hantao Zhang 001 (IJCAI, 1995)

Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results. - Mark E. Stickel; Hantao Zhang 001 (RTA, 1995)

Contextual Rewriting in Automated Reasoning. - Hantao Zhang 001 (Fundam. Informaticae, 1995)

A Path Ordering for Proving Termination of AC Rewrite Systems. - Deepak Kapur; G. Sivakumar; Hantao Zhang 001 (J. Autom. Reason., 1995)

Combining Local Search and Backtracking Techniques for Constraint Satisfaction. - Jian Zhang 001; Hantao Zhang 001 (AAAI/IAAI, Vol. 1, 1996)

System Description: Generating Models by SEM. - Jian Zhang 001; Hantao Zhang 001 (CADE, 1996)

Self-Orthogonal Mendelsohn Triple Systems. - Frank E. Bennett; Hantao Zhang 001; Lie Zhu (J. Comb. Theory A, 1996)

PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems. - Hantao Zhang 001; Maria Paola Bonacina; Jieh Hsiang (J. Symb. Comput., 1996)

SATO: An Efficient Propositional Prover. - Hantao Zhang 001 (CADE, 1997)

Existence of Incomplete Transversal Designs with Block Size Five and Any Index lambda. - R. Julian R. Abel; Charles J. Colbourn; Jianxing Yin; Hantao Zhang 001 (Des. Codes Cryptogr., 1997)

Perfect Mendelsohn Packing Designs with Block Size Five. - Frank E. Bennett; Jianxing Yin; Hantao Zhang 001; R. Julian R. Abel (Des. Codes Cryptogr., 1998)

Direct constructions for certain types of HMOLS. - R. Julian R. Abel; Hantao Zhang 001 (Discret. Math., 1998)

Workshop: Model Computation - Principles, Algorithms, Applications. - Peter Baumgartner 001; Christian G. Fermüller; Nicolas Peltier; Hantao Zhang 001 (CADE, 2000)

A few more incomplete self-orthogonal Latin squares and related designs. - R. Julian R. Abel; Frank E. Bennett; Hantao Zhang 001; Lie Zhu (Australas. J Comb., 2000)

Existence of HSOLSSOMs with type hn and 1nu1. - R. Julian R. Abel; Frank E. Bennett; Hantao Zhang 001; Lie Zhu (Ars Comb., 2000)

Implementing the Davis-Putnam Method. - Hantao Zhang 001; Mark E. Stickel (J. Autom. Reason., 2000)

Steiner pentagon covering designs. - R. Julian R. Abel; Frank E. Bennett; Hantao Zhang 001; Lie Zhu (Discret. Math., 2001)

A few more r-orthogonal latin squares. - Lie Zhu; Hantao Zhang 001 (Discret. Math., 2001)

Existence of frame SOLS of type anb1. - Yungqing Xu; Hantao Zhang 001; Lie Zhu (Discret. Math., 2002)

On approximation of max-vertex-cover. - Qiaoming Han; Yinyu Ye 001; Hantao Zhang 001; Jiawei Zhang 006 (Eur. J. Oper. Res., 2002)

Existence of self-orthogonal diagonal Latin squares with a missing subsquare. - Frank E. Bennett; Beiliang Du; Hantao Zhang 001 (Discret. Math., 2003)

Completing the spectrum of r-orthogonal Latin squares. - Lie Zhu; Hantao Zhang 001 (Discret. Math., 2003)

An Empirical Study of MAX-2-SAT Phase Transitions. - Haiou Shen; Hantao Zhang 001 (Electron. Notes Discret. Math., 2003)

Exact Algorithms for MAX-SAT. - Hantao Zhang 001; Haiou Shen; Felip Manyà (FTP, 2003)

Preface to First order theorem proving. - Peter Baumgartner 001; Hantao Zhang 001 (J. Symb. Comput., 2003)

Study of Lower Bound Functions for MAX-2-SAT. - Haiou Shen; Hantao Zhang 001 (AAAI, 2004)

Extending Finite Model Searching with Congruence Closure Computation. - Jian Zhang 001; Hantao Zhang 001 (AISC, 2004)

Improving First-order Model Searching by Propositional Reasoning and Lemma Learning. - Zhuo Huang; Hantao Zhang 001; Jian Zhang 001 (SAT, 2004)

A SAT Based Scheduler for Tournament Schedules. - Hantao Zhang 001; Dapeng Li; Haiou Shen (SAT, 2004)

Latin Squares with Self-Orthogonal Conjugates. - Frank E. Bennett; Hantao Zhang 001 (Discret. Math., 2004)

Another Complete Local Search Method for SAT. - Haiou Shen; Hantao Zhang 001 (LPAR, 2005)

Improving exact algorithms for MAX-2-SAT. - Haiou Shen; Hantao Zhang 001 (Ann. Math. Artif. Intell., 2005)

A Complete Random Jump Strategy with Guiding Paths. - Hantao Zhang 001 (SAT, 2006)

A Case Study in Engineering SQL Constraint Database Systems (Extended Abstract). - Sebastien Siva; James J. Lu; Hantao Zhang 001 (ICLP, 2008)

Existence of HSOLSSOMs of type 2nu1. - R. Julian R. Abel; Frank E. Bennett; Hantao Zhang 001 (Discret. Math., 2008)

Frame self-orthogonal Mendelsohn triple systems of type hn. - Yunqing Xu; Yanxun Chang; Gennian Ge; Hantao Zhang 001 (Discret. Math., 2008)

Constraint processing in relational database systems: from theory to implementation. - James J. Lu; Sebastien Siva; Ojas Parekh; George H. L. Fletcher; Hantao Zhang 001 (SAC, 2010)

Holey Schröder designs of type 4n u1. - Frank E. Bennett; Hantao Zhang 001 (Australas. J Comb., 2012)

Schröder quasigroups with a specified number of idempotents. - Frank E. Bennett; Hantao Zhang 001 (Discret. Math., 2012)

Quasigroups satisfying Stein's third law with a specified number of idempotents. - Frank E. Bennett; Hantao Zhang 001 (Discret. Math., 2012)

MACE4 and SEM: A Comparison of Finite Model Generators. - Hantao Zhang 001; Jian Zhang 001 (Automated Reasoning and Mathematics, 2013)

25 new rr-self-orthogonal Latin squares. - Hantao Zhang 001 (Discret. Math., 2013)

Strongly symmetric self-orthogonal diagonal Latin squares and Yang Hui type magic squares. - Yong Zhang 019; Kejun Chen; Nanyuan Cao; Hantao Zhang 001 (Discret. Math., 2014)

On Holey Schroder Designs of Type 2nu1. - Hantao Zhang 001; Stanley Ziewacz (Ars Comb., 2016)

The Existence of Irrational Diagonally Ordered Magic Squares. - H. Yu; D. Wu; Hantao Zhang 001 (Graphs Comb., 2016)

An Experiment with Satisfiability Modulo SAT. - Hantao Zhang 001 (J. Autom. Reason., 2016)

Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing. - Pei Huang 002; Feifei Ma; Cunjing Ge; Jian Zhang 001; Hantao Zhang 001 (IJCAR, 2018)

Sort race. - Hantao Zhang 001; Baoluo Meng; Yiwen Liang (Softw. Pract. Exp., 2022)

Investigating the Existence of Holey Latin Squares via Satisfiability Testing. - Minghao Liu 001; Rui Han; Fuqi Jia; Pei Huang 002; Feifei Ma; Hantao Zhang 001; Jian Zhang 001 (PRICAI (2), 2023)

Holey Schröder designs of type 3nu1. - Dianhua Wu; Hantao Zhang 001 (Discret. Math., 2023)