 | 2009 |
|---|
| 71 |       | Hantao Zhang:
Combinatorial Designs by SAT Solvers.
Handbook of Satisfiability 2009: 533-568 |
| 2008 |
|---|
| 70 | | Sebastien Siva,
James J. Lu,
Hantao Zhang:
A Case Study in Engineering SQL Constraint Database Systems (Extended Abstract).
ICLP 2008: 774-778 |
| 69 | | Yunqing Xu,
Yanxun Chang,
Gennian Ge,
Hantao Zhang:
Frame self-orthogonal Mendelsohn triple systems of type hn.
Discrete Mathematics 308(22): 5049-5063 (2008) |
| 68 | | R. Julian R. Abel,
Frank E. Bennett,
Hantao Zhang:
Existence of HSOLSSOMs of type 2nu1.
Discrete Mathematics 308(22): 5149-5173 (2008) |
| 2006 |
|---|
| 67 | | Hantao Zhang:
A Complete Random Jump Strategy with Guiding Paths.
SAT 2006: 96-101 |
| 2005 |
|---|
| 66 | | Haiou Shen,
Hantao Zhang:
Another Complete Local Search Method for SAT.
LPAR 2005: 595-605 |
| 65 | | Haiou Shen,
Hantao Zhang:
Improving exact algorithms for MAX-2-SAT.
Ann. Math. Artif. Intell. 44(4): 419-436 (2005) |
| 2004 |
|---|
| 64 |  | Haiou Shen,
Hantao Zhang:
Study of Lower Bound Functions for MAX-2-SAT.
AAAI 2004: 185-190 |
| 63 | | Jian Zhang,
Hantao Zhang:
Extending Finite Model Searching with Congruence Closure Computation.
AISC 2004: 94-102 |
| 62 | | Haiou Shen,
Hantao Zhang:
Improving Exact Algorithms for MAX-2-SAT.
AMAI 2004 |
| 61 | | Hantao Zhang,
Dapeng Li,
Haiou Shen:
A SAT Based Scheduler for Tournament Schedules.
SAT 2004 |
| 60 | | Zhuo Huang,
Hantao Zhang,
Jian Zhang:
Improving First-order Model Searching by Propositional Reasoning and Lemma Learning.
SAT 2004 |
| 59 | | Frank E. Bennett,
Hantao Zhang:
Latin Squares with Self-Orthogonal Conjugates.
Discrete Mathematics 284(1-3): 45-55 (2004) |
| 2003 |
|---|
| 58 | | Frank E. Bennett,
Beiliang Du,
Hantao Zhang:
Existence of self-orthogonal diagonal Latin squares with a missing subsquare.
Discrete Mathematics 261(1-3): 69-86 (2003) |
| 57 | | Lie Zhu,
Hantao Zhang:
Completing the spectrum of r-orthogonal Latin squares.
Discrete Mathematics 268(1-3): 343-349 (2003) |
| 56 | | Hantao Zhang,
Haiou Shen,
Felip Manyà:
Exact Algorithms for MAX-SAT.
Electr. Notes Theor. Comput. Sci. 86(1): (2003) |
| 55 | | Haiou Shen,
Hantao Zhang:
An Empirical Study of MAX-2-SAT Phase Transitions.
Electronic Notes in Discrete Mathematics 16: 80-92 (2003) |
| 54 | | Peter Baumgartner,
Hantao Zhang:
Preface to First order theorem proving.
J. Symb. Comput. 36(1-2): 1-3 (2003) |
| 2002 |
|---|
| 53 | | Hantao Zhang:
A Randomization Strategy for Combinatorial Search.
AMAI 2002 |
| 52 | | Yungqing Xu,
Hantao Zhang,
Lie Zhu:
Existence of frame SOLS of type anb1.
Discrete Mathematics 250(1-3): 211-230 (2002) |
| 51 | | Qiaoming Han,
Yinyu Ye,
Hantao Zhang,
Jiawei Zhang:
On approximation of max-vertex-cover.
European Journal of Operational Research 143(2): 342-355 (2002) |
| 2001 |
|---|
| 50 | | R. Julian R. Abel,
Frank E. Bennett,
Hantao Zhang,
Lie Zhu:
Steiner pentagon covering designs.
Discrete Mathematics 231(1-3): 11-26 (2001) |
| 49 | | Lie Zhu,
Hantao Zhang:
A few more r-orthogonal latin squares.
Discrete Mathematics 238(1-3): 183-191 (2001) |
| 2000 |
|---|
| 48 | | Peter Baumgartner,
Christian G. Fermüller,
Nicolas Peltier,
Hantao Zhang:
Workshop: Model Computation - Principles, Algorithms, Applications.
CADE 2000: 513 |
| 47 | | R. Julian R. Abel,
Frank E. Bennett,
Hantao Zhang,
Lie Zhu:
Existence of HSOLSSOMs with type hn and 1nu1.
Ars Comb. 55: (2000) |
| 46 | | Hantao Zhang,
Mark E. Stickel:
Implementing the Davis-Putnam Method.
J. Autom. Reasoning 24(1/2): 277-296 (2000) |
| 1998 |
|---|
| 45 | | Frank E. Bennett,
Jianxing Yin,
Hantao Zhang,
R. Julian R. Abel:
Perfect Mendelsohn Packing Designs with Block Size Five.
Des. Codes Cryptography 14(1): 5-22 (1998) |
| 44 | | R. Julian R. Abel,
Hantao Zhang:
Direct constructions for certain types of HMOLS.
Discrete Mathematics 181(1-3): 1-17 (1998) |
| 1997 |
|---|
| 43 | | Hantao Zhang:
SATO: An Efficient Propositional Prover.
CADE 1997: 272-275 |
| 42 | | R. Julian R. Abel,
Charles J. Colbourn,
Jianxing Yin,
Hantao Zhang:
Existence of Incomplete Transversal Designs with Block Size Five and Any Index lambda.
Des. Codes Cryptography 10(3): 275-307 (1997) |
| 1996 |
|---|
| 41 | | Jian Zhang,
Hantao Zhang:
Combining Local Search and Backtracking Techniques for Constraint Satisfaction.
AAAI/IAAI, Vol. 1 1996: 369-374 |
| 40 | | Jian Zhang,
Hantao Zhang:
System Description: Generating Models by SEM.
CADE 1996: 308-312 |
| 39 | | Frank E. Bennett,
Hantao Zhang,
Lie Zhu:
Self-Orthogonal Mendelsohn Triple Systems.
J. Comb. Theory, Ser. A 73(2): 207-218 (1996) |
| 38 | | Hantao Zhang,
Maria Paola Bonacina,
Jieh Hsiang:
PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems.
J. Symb. Comput. 21(4): 543-560 (1996) |
| 1995 |
|---|
| 37 | | Jian Zhang,
Hantao Zhang:
Constraint Propagation in Model Generation.
CP 1995: 398-414 |
| 36 | | Jian Zhang,
Hantao Zhang:
SEM: a System for Enumerating Models.
IJCAI 1995: 298-303 |
| 35 | | Mark E. Stickel,
Hantao Zhang:
Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results.
RTA 1995: 450-456 |
| 34 | | Hantao Zhang:
Contextual Rewriting in Automated Reasoning.
Fundam. Inform. 24(1/2): 107-123 (1995) |
| 33 | | Deepak Kapur,
G. Sivakumar,
Hantao Zhang:
A Path Ordering for Proving Termination of AC Rewrite Systems.
J. Autom. Reasoning 14(2): 293-316 (1995) |
| 1994 |
|---|
| 32 | | Sun Kim,
Hantao Zhang:
ModGen: Theorem Proving by Model Generation.
AAAI 1994: 162-167 |
| 31 | | Hantao Zhang:
A New Method for the Boolean Ring Based Theorem Proving.
J. Symb. Comput. 17(2): 189-211 (1994) |
| 1993 |
|---|
| 30 | | Xin Hua,
Hantao Zhang:
Formal Semantics of VHDL for Verification of Circuit Designs.
ICCD 1993: 446-449 |
| 29 | | Hantao Zhang:
A Case Study of Completion Modulo Distributivity and Abelian Groups.
RTA 1993: 32-46 |
| 28 | | Hantao Zhang,
Gary Xin Hua:
Proving Ramsey's Theorem by the Cover Set Induction: A Case and Comparison Study.
Ann. Math. Artif. Intell. 8(3-4): 383-405 (1993) |
| 27 | | Hantao Zhang:
Automated Proofs of Equality Problems in Overbeek's Competition.
J. Autom. Reasoning 11(3): 333-351 (1993) |
| 1992 |
|---|
| 26 | | Hantao Zhang,
Xin Hua:
Proving the Chinese Remainder Theorem by the Cover Set Induction.
CADE 1992: 431-445 |
| 25 | | Xin Hua,
Hantao Zhang:
FRI: Failure-Resistant Induction in RRL.
CADE 1992: 691-695 |
| 24 | | Hantao Zhang:
Herky: High Performance Rewriting in RRL.
CADE 1992: 696-700 |
| 23 | | Hantao Zhang:
Proving Group Isomorphism Theorems (Extended Abstract).
CTRS 1992: 302-306 |
| 22 | | Hantao Zhang:
Implementing Contextual Rewriting.
CTRS 1992: 363-377 |
| 1991 |
|---|
| 21 | | Hantao Zhang,
Angshuman Guha,
Xin Hua:
Using Algebraic Specification in Floyd-Hoare Assertions.
AMAST 1991: 350-362 |
| 20 | | Deepak Kapur,
Hantao Zhang:
A Case Study of the Completion Procedure: Proving Ring Commutativity Problems.
Computational Logic - Essays in Honor of Alan Robinson 1991: 360-394 |
| 19 | | Deepak Kapur,
Paliath Narendran,
Daniel J. Rosenkrantz,
Hantao Zhang:
Sufficient-Completeness, Ground-Reducibility and their Complexity.
Acta Inf. 28(4): 311-350 (1991) |
| 18 | | Deepak Kapur,
Paliath Narendran,
Hantao Zhang:
Automating Inductionless Induction Using Test Sets.
J. Symb. Comput. 11(1/2): 81-111 (1991) |
| 1990 |
|---|
| 17 | | Deepak Kapur,
G. Sivakumar,
Hantao Zhang:
A New Method for Proving Termination of AC-Rewrite Systems.
FSTTCS 1990: 133-148 |
| 16 | | Hantao Zhang:
Approximate Reasoning in Strength Logic.
ISMVL 1990: 262-269 |
| 15 | | Hantao Zhang:
Automated Proof of Ring Commutativity Problems by Algebraic Methods.
J. Symb. Comput. 9(4): 423-427 (1990) |
| 14 | | Hantao Zhang,
Deepak Kapur:
Unnecessary Inferences in Associative-Commutative Completion Procedures.
Mathematical Systems Theory 23(3): 175-206 (1990) |
| 1989 |
|---|
| 13 | | Hantao Zhang,
Deepak Kapur:
Consider Only General Superpositions in Completion Procedures.
RTA 1989: 513-527 |
| 12 | | Deepak Kapur,
Hantao Zhang:
An Overview of Rewrite Rule Laboratory (RRL).
RTA 1989: 559-563 |
| 1988 |
|---|
| 11 | | Hantao Zhang,
Deepak Kapur:
First-Order Theorem Proving Using Conditional Rewrite Rules.
CADE 1988: 1-20 |
| 10 | | Hantao Zhang,
Deepak Kapur,
Mukkai S. Krishnamoorthy:
A Mechanizable Induction Principle for Equational Specifications.
CADE 1988: 162-181 |
| 9 | | Deepak Kapur,
Hantao Zhang:
RRL: A Rewrite Rule Laboratory.
CADE 1988: 768-769 |
| 8 | | Deepak Kapur,
Hantao Zhang:
Proving Equivalence of Different Axiomatizations of Free Groups.
J. Autom. Reasoning 4(3): 331-352 (1988) |
| 7 | | Hans-Jürgen Bürckert,
Alexander Herold,
Deepak Kapur,
Jörg H. Siekmann,
Mark E. Stickel,
Michael Tepp,
Hantao Zhang:
Opening the AC-Unification Race.
J. Autom. Reasoning 4(4): 465-474 (1988) |
| 1987 |
|---|
| 6 | | Deepak Kapur,
Paliath Narendran,
Hantao Zhang:
On Sufficient-Completeness and Related Properties of Term Rewriting Systems.
Acta Inf. 24(4): 395-415 (1987) |
| 1986 |
|---|
| 5 | | Deepak Kapur,
G. Sivakumar,
Hantao Zhang:
RRL: A Rewrite Rule Laboratory.
CADE 1986: 691-692 |
| 4 | | Deepak Kapur,
Paliath Narendran,
Hantao Zhang:
Proof by Induction Using Test Sets.
CADE 1986: 99-117 |
| 3 | | Deepak Kapur,
Paliath Narendran,
Hantao Zhang:
Complexity of Sufficient-Completeness.
FSTTCS 1986: 426-442 |
| 1985 |
|---|
| 2 | | Hantao Zhang,
Jean-Luc Remy:
Contextual Rewriting.
RTA 1985: 46-62 |
| 1984 |
|---|
| 1 | | Jean-Luc Remy,
Hantao Zhang:
REVEUR 4: A System for Validating Conditional Algebraic Specifications of Abstract Data Types.
ECAI 1984: 373-382 |
