Preview
Unable to display preview. Download preview PDF.
References
Aubin R., "Mechanizing Structural induction", T.C.S. 9, 1979, pp 329–345 and 347–362.
Boyer R., Moore J.S., A computational logic, Academic press, 1979.
Burstall R.M., "Proving properties of program by structural induction", Comput. J 12, 1969, pp 41–48.
Fay M., "First-Order Unification in an Equational Theory", Proc. 4th Workshop on Automated Deduction, Austin, 1979, pp 161–167.
Fribourg L., "Refutation par Superposition de Clauses Equationnelles", These de 3eme cycle, U. Paris 7, Sept. 1982.
Fribourg L., "A Narrowing Procedure for Theories with Constructors", 7th Conf. on Automated Deduction, May 1984, pp 259–281.
Goguen J.A., "How to Prove Algebraic Inductive Hypotheses Without Induction, with Applications to the Correctness of Data Type Implementation", 5th Conf. on Automated Deduction, Les Arcs, July 1980, pp 356–373.
Hullot J.M., "Canonical Form and Unification", 5th Conf. on Automated Deduction, Les Arcs, July 1980, pp 318–334.
Huet G., Hullot J.M., "Proofs by induction in equational theories with constructors", 21st FOCS, 1980, pp 96–107
Huet G., Oppen D., "Equations and Rewrite Rules: A Survey", Formal Languages Perspective and Open Problems, Ed. Book R, Academic Press, 1980, pp 349–406
Huet G., "A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm", T.R. 25, INRIA, July 1980 (also in JCSS 23:1, Aug. 1981, pp 11–21).
Huet G., "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems" J.ACM 27:4, Oct. 1980, pp 797–821.
Jouannaud J.P., Kirchner H., "Completion of a Set of Rules Modulo a Set of Equations", Proc 11th POPL, Salt Lake City, Jan. 1984.
Jouannaud J.P., Kounalis E., "Proofs by Induction in Equational Theories Without Constructors", Bulletin of EATCS 27, Oct. 1985, pp 49–55.
Kaplan S., "Conditional Rewrite Rules", T.C.S. 33, Dec.1984, pp 175–193.
Kaplan S., "Fair Conditional Term Rewriting Systems: Unification, Termination and Confluence", TR no 194, LRI, Orsay, Nov.1984.
Knuth D., Bendix P., "Simple Word Problems in Universal Algebras", Computational Problems in Abstract Algebras, Pergamon Press, 1970, pp 263–297.
Kamin S., Levy J.-J., "Two Generalisations of the Recursive Path Ordering", Unpublished Note, Dept of Computer Science, U. Illinois, Feb. 1980.
Lankford D, "Canonical Inference", Report ATP-32, U. of Texas, 1975.
Manna Z., Ness N., "On the Termination of Markov Algorithms", Proc. 3rd Hawaii Intl. Conf. on Systems and Science, Jan. 1970, pp. 789–792.
Musser D.L., "On Proving Inductive Properties of Abstract Data Types", Proc. 7th POPL, Las Vegas, 1980, pp 154–162.
Peterson G., Stickel M.E., "Complete Sets of Reductions for Some Equational Theories", J.ACM 28, 1981, pp 233–264.
Remy J.L. "Etude des Systemes de Reecriture Conditionnels et Application aux Types Abstraits Algebriques", These d'Etat, Nancy, 1982.
Remy J.L., Zhang H., "REVEUR4: A System for Validating Conditional Algebraic Specifications of Abstract Data Types", Proc. ECAI, Pisa, 1984, pp 563–572.
Slagle J.R., "Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity", J.ACM 21:4, Oct 1974, pp 622–642.
Smith D.R., "Reasoning by Cases and the Formation of Conditional Programs", Intl. Joint Conf. on Artificial Intelligence, Los Angeles., Aug. 1985, pp. 215–218.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fribourg, L. (1986). A Strong restriction of the inductive completion procedure. In: Kott, L. (eds) Automata, Languages and Programming. ICALP 1986. Lecture Notes in Computer Science, vol 226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16761-7_60
Download citation
DOI: https://doi.org/10.1007/3-540-16761-7_60
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16761-7
Online ISBN: 978-3-540-39859-2
eBook Packages: Springer Book Archive