Grossly out of date.
Reflects only pre-1996 work.
No time to update, sorry.
All recent papers are in postscript
form and are available upon request at
hsiang@csie.ntu.edu.tw
[Books]
L. Bachmair J. Hsiang, editors,
Rewrite Techniques in Theorem Proving,
Academic Press, London, 1991.
J. Hsiang, editor,
Rewrite Techniques and Applications, 439 pages,
Lecture Notes in Computer Science, volume 940,
Springer-Verlag, 1995.
[Journal Publications]
J. Hsiang,
``Refutational Theorem Proving using Term Rewriting Systems'',
Artificial Intelligence Journal, Vol 25, pp255--300, 1985.
Translated into Russian and included in
Cybernetics Annual, 25 (1988) pp. 5--57, Academic of Science, Moscow.
J. Hsiang,
``Rewrite Method for Theorem Proving in First Order Theory with Equality'',
Journal of Symbolic Computation,
Vol 3, pp133--151, 1987.
J. Hsiang M.K. Srivas,
``Automatic Inductive Theorem Proving using Prolog'',
Theoretical Computer Science, Vol 54, no. 1, pp3--28, 1987.
S. Anantharaman J. Hsiang,
``Automated Proofs of the Moufang Identities in Alternative Rings'',
Journal of Automated Reasoning, vol. 6, pp79-109, 1990.
J. Hsiang M. Rusinowitch,
``Proving Refutational Completeness of Theorem Proving Strategies.
The Transfinite Semantic Tree Method'',
Journal of ACM, vol 38, pp 559--587, July, 1991.
J. Hsiang, H. Kirchner, P. Lescanne, M. Rusinowitch,
``Automated Theorem Proving in the Presence of Equalities'',
Journal of Logic Programming, Volume 14, No. 12, pp71--100, 1992.
M.P. Bonacina J. Hsiang,
``On Rewrite Programs: Semantics and Relationship with Prolog'',
Journal of Logic Programming, Volume 14, No. 12, pp155--180, 1992.
M.P. Bonacina J. Hsiang,
``On Subsumption in Distributed Deduction'',
Journal of Automated Deduction, vol 12, pp 225-240, 1994.
M.P. Bonacina J. Hsiang,
``Parallelizing deduction strategies: an analytical study'',
Journal of Automated Reasoning, vol 13, pp 1--33, 1994.
M.P. Bonacina J. Hsiang,
``Towards a Foundation of Completion Procedures as Semidecision Procedures'',
Theoretical Computer Science
Vol. 146, 199--242, July 1995.
M.P. Bonacina J. Hsiang,
``Distributed Deduction by Clause-Diffusion'',
Fundamenta Informaticae, Vol. 24, 177--207, September 1995.
M.P. Bonacina J. Hsiang,
``Distributed Deduction by Clause-Diffusion:
Distributed Contraction and the Aquarius Prover'',
Journal of Symbolic Computation, vol 19, pp 245--267, 1995.
H. Chen J. Hsiang,
``Recurrence Domains: Their Unification and Application to Logic Programming'',
Information and Computation vol 122, pp 45--69, 1995.
M.P. Bonacina J. Hsiang,
``A category theory approach to completion-based theorem proving strategies'',
23 pages, accepted and to appear in
Journal of Information Science and Engineering.
H. Zhang, M.P. Bonacina J. Hsiang,
``PSATO: a Distributed Propositional Prover and
Its Application to Quasigroup Problem'',
to appear in Journal of Symbolic Computation, 1996.
J. Hsiang A. Wasilewska,
``Automating Algebraic Proofs in Algebraic Logic'',
to appear in Fundamenta Informaticae, September, 1996.
J. Hsiang J. Mzali,
``Algorithme de Completion SKB'' (in French),
accepted upon revision, RAIRO, Informatique Theorique.
H. Chen J. Hsiang,
``Order-sorted Specification and Completion'', 37 pages,
accepted upon revision in Journal of Symbolic Computation.
[Papers in Referreed Conference Proceedings]
J. Hsiang N. Dershowitz,
``Rewrite Methods for Clausal and Nonclausal Theorem Proving'',
the Proceedings of the
10th International Conference on Automata, Languages and Programming,
Barcelona, Spain, 1983, Springer-Verlag Lecture
Notes in Computer Science, Vol 154, pp331--346.
N. Dershowitz, J. Hsiang, N. Josephson, D. Plaisted,
``Associative-Commutative Rewriting'',
the Proceedings of the
8th International Joint Conf. on Artificial Intelligence,
pp940--944, Karlsruhe, Germany, August 1983.
J. Hsiang M.K. Srivas,
``A Prolog Environment for Developing and Reasoning about Data Types'',
the Proceedings of the
Colloquium on Software Engineering (TAPSOFT)
Berlin, March 1985.
Springer-Verlag Lecture Notes in Computer Science, Vol 186, pp276--293.
J. Hsiang,
``Two Results in Term Rewriting Theorem Proving'',
Rewriting Techniques and Applications,
Springer-Verlag Lecture Notes in Computer Science, Vol 202, pp310--324,
May 1985.
J. Hsiang M.K. Srivas,
``Prolog-based Inductive Theorem Proving",
the Proceedings of the
5th Foundations of Software Technology and Theoretical Computer Science
Dec. 1985.
Springer-Verlag Lecture Notes in Computer Science, Vol 206, pp129--149.
L. Bachmair, N. Dershowitz, J. Hsiang,
``Orderings for Equational Proofs'',
Proceedings of the
Symposium on Logic in Computer Science,
Boston, June, 1986.
J. Hsiang M. Rusinowitch,
``A New Method for Establishing Refutational Completeness in Theorem
Proving'',
Proceedings of the
8th Conference on Automated Deduction,
July, 1986.
Springer-Verlag Lecture Notes in Computer Science, Vol 230, pp141--152.
J. Hsiang M. Rusinowitch,
``On Word Problems in Equational Theories'',
14th International Conference on Automata, Languages and Programming,
Karlsruhe, Germany, July, 1987.
Springer-Verlag Lecture Notes in Computer Science, Vol 267, pp54--71.
J. Hsiang, M. Rusinowitch, K. Sakai,
``Complete Set of Inference Rules for the Cancellation Laws'',
10th International Joint Conf. on Artificial Intelligence,
Milan, Italy, August, 1987.
J. Hsiang J.-P. Jouannaud,
``Complete Sets of Inference Rule for E-Unifications'',
2nd International Workshop on Unification, Val d'Ajol, France, 1988.
S. Anantharaman, J. Hsiang, J. Mzali,
``SbReve: A Term Rewriting Laboratory with Unfailing Completion'',
3rd International Conference on Rewrite
Techniques and Applications, April, 1989.
H. Chen, J. Hsiang H.C. Kung,
``On finite representation of infinite terms'',
the proceedings of the
2nd International Conference on Conditional Term
Rewriting Systems, Montreal, May, 1990.
M.P. Bonacina J. Hsiang,
``Completion Procedures as Semi-Decision Procedures'',
the proceedings of the
2nd International Conference on Conditional Term
Rewriting Systems, Montreal, May, 1990.
M.P. Bonacina J. Hsiang,
``Operational and Denotational Semantics of Rewrite Programs'',
North American Conference in Logic Programming,
Austin, Texas, October, 1990.
M.P. Bonacina J. Hsiang,
``On Fairness of Completion-based Theorem Proving Strategies'',
in R.V. Book (ed.),
Proceedings of the Fourth International Conference on
Rewriting Techniques and Applications, Como, Italy, April 1991,
Springer Verlag,
Lecture Notes in Computer Science 488,
pp348--360, April 1991.
M.P. Bonacina J. Hsiang,
``High Performance Simplification-based Automated Deduction'',
in Transactions of the Ninth Army Conference on
Applied Mathematics and
Computing, Minneapolis, Minnesota, June 1991,
ARO Report 92-1, 321--335, March 1992.
M.P. Bonacina J. Hsiang,
``A Category Theory Approach to Completion-based Theorem Proving Strategies'',
CATEGORY THEORY 91', Montreal, June 1991.
H. Chen J. Hsiang,
``Logic Programming with Recurrence Domains'',
18th International Conference on Automata, Languages and Programming,
Madrid, July, 1991.
M.P. Bonacina J. Hsiang,
``A System for Distributed Simplification-Based Theorem Proving'',
in the proceedings of Parallel Deduction Systems, Springer-Verlag
LNCS, 1992.
M.P. Bonacina J. Hsiang,
``On fairness in distributed automated deduction'',
in P.Enjalbert, A.Finkel and K.W.Wagner (eds.),
Proceedings of the Tenth Symposium on Theoretical
Aspects of Computer Science, Wurzburg, Germany,
February 1993, Springer Verlag, Lecture Notes in
Computer Science 665, 141--152, 1993.
M.P. Bonacina J. Hsiang,
``Distributed Deduction by Clause-Diffusion:
the Aquarius Prover''
in the proceedings of the third conference on the Design and Implementation
of Symbolic Computation,
Gmunden, Austria,
September 1993, Springer Verlag, Lecture Notes
in Computer Science 722, 272--287, 1993.
J. Hsiang,
``Verification sequential circuits using inductive theorem proving'',
proceedings of the Workshop on Inductive Theorem Proving,
Nancy, France, June 1994.
H. Zhang J. Hsiang,
``Solving open problems in quasigroups by propositional reasoning'',
proceedings of International Computer Science Conference,
Hsin-Chu, Taiwan, December, 1994.
J. Hsiang J.S. Lee,
``Generic Virus Detection and Pattern Generation'',
proceedings of the conference Virus Bulletin, Boston, September, 1995.
J. Hsiang K.S. Huang,
``On Boolean Ring Normal Forms'',
DIMACS Workshop on Satisfiability Problems, March, 1996.
M.P. Bonacina, J. Hsiang,
``On Semantic Resolution with Lemmaizing and Contraction'',
PRICAI, August, 1996.
[Abstracts]
J. Hsiang N.A. Josephson,
``TeRSe: A Term Rewriting Theorem prover'',
the Proceedings of
The Rewrite Rule Laboratory Workshop,
General Electric Research and Development Center, Schenectady, NY 12345.
September 6--9, 1983
J. Hsiang,
``Term Rewriting Theorem Proving for Equality'',
the Proceedings of the
Workshop in Combinatorial Algorithms in Algebraic Structures,
Otzenhausen, Germany, August, 1985.
N. Dershowitz J. Hsiang
``Refutational Theorem Proving with Oriented Equations",
Colloquium on the Resolution of Equations in Algebraic Structures',
Lakeway, Texas, May 1987.
J. Hsiang,
``Knuth-Bendix Completion as a Semi-Decision Procedure'',
the proceedings of
The First International Workshop of Conditional Term Rewriting Method,
June, 1987.
H. Chen J. Hsiang,
``Computing with Recurrence Domains'',
Symposium on Theoretical Computer Science, Toyohashi, Japan, August, 1990.
J. Hsiang,
``Simplification Orderings as a basis for Automated Deduction'',
U.S./Japan Workshop on Automated Deduction, Argonne, June 1991.
M.P. Bonacina J. Hsiang,
``Incompleteness of the RUE/NRF inference systems'',
Association of Automated Reasoning Newsletter, 1991.