Transformation d'une preuve réduite en une preuve par expansion pour une formule plus grande par la relation ,
IILl Règles de mise en forme anti-prénexe ,
un quantificateur existentiel pour la mise en forme prénexe d'une preuve o ? ,
-Refutations by Matings, IEEE Transactions and Computers, vol.8, pp.801-807, 1976. ,
-Transforming Mmatings into N atural Deduction Proofs, ln: Proceedings 5th International Conference on A utomated Deduction, Les Arcs (France), pp.281-292 ,
Cooper (8.) et Pierce (W.). -Analogical Reasoning and Proof Discovery, Proceedings 9th International Conference on Automated Deduction, pp.454-468, 1988. ,
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
-A Science of Reasoning. ln: Computational logic : essays in honor of Alan Robinson, éd, pp.178-198 ,
-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 ,
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
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
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
-A calculus for proofs and proof generalization ,
Roger) et Seldin (Johnathan P.). -Introduction to Combinators and Lambda-calculus, 1986. ,
-Résolution d'equations dans les langages d'ordre 1, Thèse de Doctorat d'Etat, 1976. ,
A paradigm for reasoning by analogy, Artificial Intelligence, vol.2, issue.2, pp.147-178, 1971. ,
DOI : 10.1016/0004-3702(71)90008-7
-Reusing proofs, I1th European Conference on Artificial Intelligence, éd. par Cohn (A.), pp.80-84, 1994. ,
-Analogies between proofs -a case study, Rapport technique, U niversitat des Saarlandes, 1993. ,
-Change of Representation in Theor'em Proving by Analogy. -Rapport technique n° SR-93-07, 1993. ,
A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987. ,
DOI : 10.1007/978-3-642-86718-7
-Theory and practice of modular higher-order Eunification, Proceedings 12th International Conference on A utomated Deduction, pp.650-664, 1994. ,
-Combining mat ching algorithms: The regular case, Journal of Symbolic Computation, pp.633-653, 1991. ,
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
-Analogy for Automated reasoning, Perspectives in Artificial Intelligence, 1990. ,
-Analytic and Non-analytic Proofs, Proceedings 7th International Conference on Automated Deduction, pp.394-413, 1984. ,
-Prao! Transformation in Higher-Order Logic, 1987. ,
Theorem proving with abstraction, Artificial Intelligence, vol.16, issue.1, pp.47-108, 1981. ,
DOI : 10.1016/0004-3702(81)90015-1
-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
-Higher-order E-unification for arbitrary theories, LOGIC PROGRAMMING : Proceedings of 1992 joint international conference and symposium on logic programming, éd. par Apt, 1992. ,
-Complete Sets of Transformations for General Unification ,
-Boolean Simplification of First-Order Formulae. -SEKI-Report n° SR-87 -04, 1987. ,