# Hantao Zhang

According to our database

^{1}, Hantao Zhang## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### On csauthors.net:

## Bibliography

2016

An Experiment with Satisfiability Modulo SAT.

J. Autom. Reasoning, 2016

Sort Race.

CoRR, 2016

On Holey Schroder Designs of Type 2

^{n}u^{1}.
Ars Comb., 2016

2014

Strongly symmetric self-orthogonal diagonal Latin squares and Yang Hui type magic squares.

Discrete Mathematics, 2014

2013

25 new

*r*r-self-orthogonal Latin squares.
Discrete Mathematics, 2013

MACE4 and SEM: A Comparison of Finite Model Generators.

Proceedings of the Automated Reasoning and Mathematics, 2013

2012

Quasigroups satisfying Stein's third law with a specified number of idempotents.

Discrete Mathematics, 2012

Schröder quasigroups with a specified number of idempotents.

Discrete Mathematics, 2012

Australasian J. Combinatorics, 2012

2010

Constraint processing in relational database systems: from theory to implementation.

Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), 2010

2009

Combinatorial Designs by SAT Solvers.

Proceedings of the Handbook of Satisfiability, 2009

2008

Frame self-orthogonal Mendelsohn triple systems of type h

^{n}.
Discrete Mathematics, 2008

Discrete Mathematics, 2008

A Case Study in Engineering SQL Constraint Database Systems (Extended Abstract).

Proceedings of the Logic Programming, 24th International Conference, 2008

2006

A Complete Random Jump Strategy with Guiding Paths.

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

2005

Improving exact algorithms for MAX-2-SAT.

Ann. Math. Artif. Intell., 2005

Another Complete Local Search Method for SAT.

Proceedings of the Logic for Programming, 2005

2004

Latin Squares with Self-Orthogonal Conjugates.

Discrete Mathematics, 2004

A SAT Based Scheduler for Tournament Schedules.

Proceedings of the SAT 2004, 2004

Improving First-order Model Searching by Propositional Reasoning and Lemma Learning.

Proceedings of the SAT 2004, 2004

Improving Exact Algorithms for MAX-2-SAT.

Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2004

Extending Finite Model Searching with Congruence Closure Computation.

Proceedings of the Artificial Intelligence and Symbolic Computation, 2004

Study of Lower Bound Functions for MAX-2-SAT.

Proceedings of the Nineteenth National Conference on Artificial Intelligence, 2004

2003

Preface to First order theorem proving.

J. Symb. Comput., 2003

Exact Algorithms for MAX-SAT.

Electr. Notes Theor. Comput. Sci., 2003

An Empirical Study of MAX-2-SAT Phase Transitions.

Electronic Notes in Discrete Mathematics, 2003

Completing the spectrum of r-orthogonal Latin squares.

Discrete Mathematics, 2003

Existence of self-orthogonal diagonal Latin squares with a missing subsquare.

Discrete Mathematics, 2003

2002

On approximation of max-vertex-cover.

European Journal of Operational Research, 2002

Discrete Mathematics, 2002

A Randomization Strategy for Combinatorial Search.

Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2002

2001

A few more

*r*-orthogonal latin squares.
Discrete Mathematics, 2001

Steiner pentagon covering designs.

Discrete Mathematics, 2001

2000

Implementing the Davis-Putnam Method.

J. Autom. Reasoning, 2000

Existence of HSOLSSOMs with type h

^{n}and 1^{n}u^{1}.
Ars Comb., 2000

A few more incomplete self-orthogonal Latin squares and related designs.

Australasian J. Combinatorics, 2000

Workshop: Model Computation - Principles, Algorithms, Applications.

Proceedings of the Automated Deduction, 2000

1998

Direct constructions for certain types of HMOLS.

Discrete Mathematics, 1998

Perfect Mendelsohn Packing Designs with Block Size Five.

Des. Codes Cryptography, 1998

1997

Existence of Incomplete Transversal Designs with Block Size Five and Any Index lambda.

Des. Codes Cryptography, 1997

SATO: An Efficient Propositional Prover.

Proceedings of the Automated Deduction, 1997

1996

PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems.

J. Symb. Comput., 1996

Self-Orthogonal Mendelsohn Triple Systems.

J. Comb. Theory, Ser. A, 1996

System Description: Generating Models by SEM.

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Combining Local Search and Backtracking Techniques for Constraint Satisfaction.

Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, 1996

1995

A Path Ordering for Proving Termination of AC Rewrite Systems.

J. Autom. Reasoning, 1995

Contextual Rewriting in Automated Reasoning.

Fundam. Inform., 1995

Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results.

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

SEM: a System for Enumerating Models.

Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, 1995

Constraint Propagation in Model Generation.

Proceedings of the Principles and Practice of Constraint Programming, 1995

1994

A New Method for the Boolean Ring Based Theorem Proving.

J. Symb. Comput., 1994

ModGen: Theorem Proving by Model Generation.

Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31, 1994

1993

Automated Proofs of Equality Problems in Overbeek's Competition.

J. Autom. Reasoning, 1993

Proving Ramsey's Theorem by the Cover Set Induction: A Case and Comparison Study.

Ann. Math. Artif. Intell., 1993

A Case Study of Completion Modulo Distributivity and Abelian Groups.

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Formal Semantics of VHDL for Verification of Circuit Designs.

Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993

1992

Axiomatic semantics of a hardware specification language.

Proceedings of the Second Great Lakes Symposium on VLSI, 1992

Implementing Contextual Rewriting.

Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Proving Group Isomorphism Theorems (Extended Abstract).

Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Proving the Chinese Remainder Theorem by the Cover Set Induction.

Proceedings of the Automated Deduction, 1992

Herky: High Performance Rewriting in RRL.

Proceedings of the Automated Deduction, 1992

FRI: Failure-Resistant Induction in RRL.

Proceedings of the Automated Deduction, 1992

1991

Automating Inductionless Induction Using Test Sets.

J. Symb. Comput., 1991

Sufficient-Completeness, Ground-Reducibility and their Complexity.

Acta Inf., 1991

A Case Study of the Completion Procedure: Proving Ring Commutativity Problems.

Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

Using Algebraic Specification in Floyd-Hoare Assertions.

Proceedings of the Algebraic Methodology and Software Technology (AMAST '91), 1991

1990

Unnecessary Inferences in Associative-Commutative Completion Procedures.

Mathematical Systems Theory, 1990

Automated Proof of Ring Commutativity Problems by Algebraic Methods.

J. Symb. Comput., 1990

Approximate Reasoning in Strength Logic.

Proceedings of the 20th International Symposium on Multiple-Valued Logic, 1990

A New Method for Proving Termination of AC-Rewrite Systems.

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1990

1989

Consider Only General Superpositions in Completion Procedures.

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

An Overview of Rewrite Rule Laboratory (RRL).

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

1988

Proving Equivalence of Different Axiomatizations of Free Groups.

J. Autom. Reasoning, 1988

Opening the AC-Unification Race.

J. Autom. Reasoning, 1988

A Mechanizable Induction Principle for Equational Specifications.

Proceedings of the 9th International Conference on Automated Deduction, 1988

First-Order Theorem Proving Using Conditional Rewrite Rules.

Proceedings of the 9th International Conference on Automated Deduction, 1988

RRL: A Rewrite Rule Laboratory.

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

On Sufficient-Completeness and Related Properties of Term Rewriting Systems.

Acta Inf., 1987

1986

Complexity of Sufficient-Completeness.

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1986

RRL: A Rewrite Rule Laboratory.

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

Proof by Induction Using Test Sets.

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

Contextual Rewriting.

Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985

1984

REVEUR 4: A System for Validating Conditional Algebraic Specifications of Abstract Data Types.

ECAI, 1984