2008 |
70 | EE | Sebastien Siva,
James J. Lu,
Hantao Zhang:
A Case Study in Engineering SQL Constraint Database Systems (Extended Abstract).
ICLP 2008: 774-778 |
69 | EE | 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 | EE | R. Julian R. Abel,
Frank E. Bennett,
Hantao Zhang:
Existence of HSOLSSOMs of type 2nu1.
Discrete Mathematics 308(22): 5149-5173 (2008) |
2006 |
67 | EE | Hantao Zhang:
A Complete Random Jump Strategy with Guiding Paths.
SAT 2006: 96-101 |
2005 |
66 | EE | Haiou Shen,
Hantao Zhang:
Another Complete Local Search Method for SAT.
LPAR 2005: 595-605 |
65 | EE | 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 | EE | Jian Zhang,
Hantao Zhang:
Extending Finite Model Searching with Congruence Closure Computation.
AISC 2004: 94-102 |
62 | EE | Haiou Shen,
Hantao Zhang:
Improving Exact Algorithms for MAX-2-SAT.
AMAI 2004 |
61 | EE | Hantao Zhang,
Dapeng Li,
Haiou Shen:
A SAT Based Scheduler for Tournament Schedules.
SAT 2004 |
60 | EE | Zhuo Huang,
Hantao Zhang,
Jian Zhang:
Improving First-order Model Searching by Propositional Reasoning and Lemma Learning.
SAT 2004 |
59 | EE | Frank E. Bennett,
Hantao Zhang:
Latin Squares with Self-Orthogonal Conjugates.
Discrete Mathematics 284(1-3): 45-55 (2004) |
2003 |
58 | EE | 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 | EE | Lie Zhu,
Hantao Zhang:
Completing the spectrum of r-orthogonal Latin squares.
Discrete Mathematics 268(1-3): 343-349 (2003) |
56 | EE | Hantao Zhang,
Haiou Shen,
Felip Manyà:
Exact Algorithms for MAX-SAT.
Electr. Notes Theor. Comput. Sci. 86(1): (2003) |
55 | EE | Haiou Shen,
Hantao Zhang:
An Empirical Study of MAX-2-SAT Phase Transitions.
Electronic Notes in Discrete Mathematics 16: 80-92 (2003) |
54 | EE | Peter Baumgartner,
Hantao Zhang:
Preface to First order theorem proving.
J. Symb. Comput. 36(1-2): 1-3 (2003) |
2002 |
53 | EE | Hantao Zhang:
A Randomization Strategy for Combinatorial Search.
AMAI 2002 |
52 | EE | Yungqing Xu,
Hantao Zhang,
Lie Zhu:
Existence of frame SOLS of type anb1.
Discrete Mathematics 250(1-3): 211-230 (2002) |
51 | EE | 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 | EE | R. Julian R. Abel,
Frank E. Bennett,
Hantao Zhang,
Lie Zhu:
Steiner pentagon covering designs.
Discrete Mathematics 231(1-3): 11-26 (2001) |
49 | EE | 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 | EE | 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 | EE | 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 |