~. @bullet, Transformation d'une preuve réduite en une preuve par expansion pour une formule plus grande par la relation

@. @bullet, @. @bullet, . @bullet, and . @bullet, IILl Règles de mise en forme anti-prénexe

I. Remontée-d and @. @bullet, un quantificateur existentiel pour la mise en forme prénexe d'une preuve o ?

. And76 and . Andrews, -Refutations by Matings, IEEE Transactions and Computers, vol.8, pp.801-807, 1976.

. Ands7 and . Andrews, -Transforming Mmatings into N atural Deduction Proofs, ln: Proceedings 5th International Conference on A utomated Deduction, Les Arcs (France), pp.281-292

. Brock, Cooper (8.) et Pierce (W.). -Analogical Reasoning and Proof Discovery, Proceedings 9th International Conference on Automated Deduction, pp.454-468, 1988.

. Breazu-tannen, Combining algebra and higher-order types, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.82-90, 1988.
DOI : 10.1109/LICS.1988.5103

. Bundy, -A Science of Reasoning. ln: Computational logic : essays in honor of Alan Robinson, éd, pp.178-198

. Davis, -Eliminating the irrelevant from mathematical proofs In: Experimental arithmetie, High Speed Computing and Mathematies, Proeeeding of Symposia in Applied Mathematics XV. Amerîcan Mathematical Society, pp.15-30

. Dowek, Third order matching is decidable, Annals of Pure and Applied Logic, vol.69, issue.2-3, pp.135-155, 1994.
DOI : 10.1016/0168-0072(94)90083-3

. Egly, On the value of antiprenexing, ln: Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, LPAR'94, éd. par Pfenning (F.), pp.69-83, 1994.
DOI : 10.1007/3-540-58216-9_30

(. A. Felty and . Howe, Generalization and reuse of tactic proofs, Proceedîngs of the 5th International Conference on Logic Programming and A utomated Reasoning, LPAR éd. par Pfenning (F.), pp.1-15, 1994.
DOI : 10.1007/3-540-58216-9_25

. Gunter, -A calculus for proofs and proof generalization

. Hindley, Roger) et Seldin (Johnathan P.). -Introduction to Combinators and Lambda-calculus, 1986.

. Huet, -Résolution d'equations dans les langages d'ordre 1, Thèse de Doctorat d'Etat, 1976.

R. E. Kling, A paradigm for reasoning by analogy, Artificial Intelligence, vol.2, issue.2, pp.147-178, 1971.
DOI : 10.1016/0004-3702(71)90008-7

(. T. Kolbe and . Walther, -Reusing proofs, I1th European Conference on Artificial Intelligence, éd. par Cohn (A.), pp.80-84, 1994.

(. E. Meus, -Analogies between proofs -a case study, Rapport technique, U niversitat des Saarlandes, 1993.

(. E. Melis, -Change of Representation in Theor'em Proving by Analogy. -Rapport technique n° SR-93-07, 1993.

. Miller, A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987.
DOI : 10.1007/978-3-642-86718-7

(. O. Müller and . Weber, -Theory and practice of modular higher-order Eunification, Proceedings 12th International Conference on A utomated Deduction, pp.650-664, 1994.

C. Nipkow, -Combining mat ching algorithms: The regular case, Journal of Symbolic Computation, pp.633-653, 1991.

(. T. Nipkow and . Et-qian, Modular higher-order E-unification, Proceedings 4th Conference on Rewriting Techniques and Applications, pp.200-214, 1991.
DOI : 10.1007/3-540-53904-2_97

. Owen, -Analogy for Automated reasoning, Perspectives in Artificial Intelligence, 1990.

. Pfenning, -Analytic and Non-analytic Proofs, Proceedings 7th International Conference on Automated Deduction, pp.394-413, 1984.

. Pfenning, -Prao! Transformation in Higher-Order Logic, 1987.

(. D. Plaisted, Theorem proving with abstraction, Artificial Intelligence, vol.16, issue.1, pp.47-108, 1981.
DOI : 10.1016/0004-3702(81)90015-1

. Prehofer, -Decidable Higher-Horder Unification Problerns, Proceedings 12th International Conference on Automated Deduction, pp.635-649, 1994.
DOI : 10.1007/3-540-58156-1_46

URL : http://www4.in.tum.de/publ/papers/Prehofer-CADE1994.pdf

. Qian, -Higher-order E-unification for arbitrary theories, LOGIC PROGRAMMING : Proceedings of 1992 joint international conference and symposium on logic programming, éd. par Apt, 1992.

(. W. Snyder, -Complete Sets of Transformations for General Unification

(. R. Socher, -Boolean Simplification of First-Order Formulae. -SEKI-Report n° SR-87 -04, 1987.