{"id":22,"date":"2016-04-29T15:49:57","date_gmt":"2016-04-29T14:49:57","guid":{"rendered":"http:\/\/lig-membres.imag.fr\/boydelat\/?page_id=22"},"modified":"2025-02-07T10:32:07","modified_gmt":"2025-02-07T09:32:07","slug":"publications","status":"publish","type":"page","link":"https:\/\/lig-membres.imag.fr\/boydelat\/publications\/","title":{"rendered":"Publications"},"content":{"rendered":"<p>(page en construction)<\/p>\n<p>&nbsp;<\/p>\n<ul>\n<li>Thierry Boy de la Tour and Nicolas Peltier. Proof generalization in LK by second order unifier minimization. <em>Journal of Automated Reasoning<\/em>, pages 1-36, 2016. <a href=\"http:\/\/dx.doi.org\/10.1007\/s10817-016-9367-3\">published online<\/a><\/li>\n<li>Thierry Boy de la Tour and Nicolas Peltier. Analogy in automated deduction: A survey. In Henri Prade and Gilles Richard, editors, <em>Computational Approaches to Analogical Reasoning: Current Trends<\/em>, volume 548 of <em>Studies in Computational Intelligence<\/em>, pages 103-130. Springer, 2014.<\/li>\n<li>Thierry Boy de la Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, and Camilla Schwind. <em>D\u00e9duction Automatique<\/em>, volume 2 of <em>Panorama de l&#8217;Intelligence Artificielle<\/em>, chapter 3. C\u00e9padu\u00e8s, 2014.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. Solving linear constraints in elementary abelian p-groups of symmetries. <em>CoRR<\/em>, abs\/1107.4553, 2011.<\/li>\n<li>Thierry Boy de la Tour, Mnacho Echenim, and Paliath Narendran. Unification and matching modulo leaf-permutative equational presentations. In A. Armando, P. Baumgartner, and G. Dowek, editors, <em>4th International Joint Conference, IJCAR 2008<\/em>, LNAI 5195, pages 332-347, Sydney, Australia, August 2008. Springer Verlag.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. Determining unify-stable presentations. In Franz Baader, editor, <em>18th International Conference on Rewriting Techniques and Applications, RTA 2007<\/em>, Lecture Notes In Computer Science 4533, Paris, France, June 2007. Springer Verlag.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. Permutative rewriting and unification. <em>Information and Computation<\/em>, 25(4):624-650, april 2007.<\/li>\n<li>Thierry Boy de la Tour and Prakash Countcham. An isomorph-free SEM-like enumeration of models. In Maria Paola Bonacina and Thierry Boy de la Tour, editors, <em>Proceedings of the 5th International Workshop on Strategies in Automated Deduction (Strategies 2004)<\/em>, volume 125 of <em>Electronic Notes in Theoretical Computer Science<\/em>, pages 91-113. Elsevier, 15 march 2005.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. Unification in a class of permutative theories. In J\u00fcrgen Giesl, editor, <em>16th International Conference on Rewriting Techniques and Applications, RTA 2005<\/em>, Lecture Notes In Computer Science 3467, pages 105-119, Nara, Japan, april 2005. Springer Verlag.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. On the complexity of deduction modulo leaf permutative equations. <em>Journal of Automated Reasoning<\/em>, 33(3-4):271-317, October 2004.<\/li>\n<li>Thierry Boy de la Tour and Prakash Countcham. An isomorph-free sem-like enumeration of models. In Maria Paola Bonacina and Thierry Boy de la Tour, editors, <em>Fifth Workshop on Strategies in Automated Deduction<\/em>, pages 41-51, Cork, Ireland, july 2004. University College Cork.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. Overlapping leaf permutative equations. In David Basin and Micha\u00ebl Rusinowitch, editors, <em>Second International Joint Conference on Automated Reasoning, IJCAR 2004<\/em>, Lecture Notes In Artificial Intelligence 3097, pages 430-444, Cork, Ireland, july 2004. Springer Verlag.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. Np-completeness results for deductive problems on stratified terms. In Moshe Vardi and Andrei Voronkov, editors, <em>10th International Conference on Logic Programming and Automated Reasoning LPAR<\/em>, Lecture Notes In Artificial Intelligence 2850, pages 315-329, Almaty, Kazakhstan, september 2003. Springer Verlag.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. On leaf permutative theories and occurrence permutation groups. In Ingo Dahn and Laurent Vigneron, editors, <em>4th International Workshop on First-Order Theorem Proving FTP&#8217;2003<\/em>, volume 86 of <em>Electronic Notes in Theoretical Computer Science<\/em>, Valencia, spain, may 2003. Elsevier.<\/li>\n<li>Thierry Boy de la Tour and Mnacho Echenim. On leaf permutative theories and occurrence permutation groups. In Ingo Dahn and Laurent Vigneron, editors, <em>4th International Workshop on First-Order Theorem Proving FTP&#8217;2003<\/em>, Valencia, spain, june 2003. Technical Report DSIC-II\/10\/03.<\/li>\n<li>Thierry Boy de la Tour. A note on symmetry heuristics in SEM. In Andrei Voronkov, editor, <em>Proceedings of the 18th Conference on Automated Deduction CADE-18<\/em>, Lecture Notes in Artificial Intelligence 2392, pages 181-194, Copenhagen, Denmark, july 2002. Springer Verlag.<\/li>\n<li>Thierry Boy de la Tour. Some techniques of isomorph-free search. In <em>Artificial Intelligence and Symbolic Computation, International Conference AISC&#8217;2000<\/em>, pages 240-252. Springer Verlag, 2000. Lecture Notes in Artificial Intelligence 1930.<\/li>\n<li>Thierry Boy de la Tour. On the complexity of finite sorted algebras. In Ricardo Caferra and Gernot Salzer, editors, <em>Automated Deduction in Classical and Non-Classical Logics<\/em>, Lecture Notes in Artificial Intelligence 1761, pages 95-108. Springer Verlag, 2000.<\/li>\n<li>Thierry Boy de la Tour, St\u00e9phane F\u00e9vre, and Dongming Wang. Clifford term rewriting for geometric reasoning in 3d. In Xiaoshan Gao, Dongming Wang, and Lu Yang, editors, <em>Automated Deduction in Geometry (ADG&#8217;98)<\/em>, Lecture Notes in Artificial Intelligence 1669, pages 130-155. Springer Verlag, 1999.<\/li>\n<li>Thierry Boy de la Tour. How complex is a finite first-order sorted interpretation? In Ricardo Caferra and Gernot Salzer, editors, <em>FTP&#8217;98 International Workshop on First-Order Theorem Proving<\/em>, pages 76-85, Vienne, Autriche, nov 1998. Technical Report E1852-GS-981 TU Wien.<\/li>\n<li>Thierry Boy de la Tour. Up-to-isomorphism enumeration of finite models &#8211; the monadic case. In Maria Paola Bonacina and Ulrich Furbach, editors, <em>FTP97 International Workshop First-Order Theorem Proving<\/em>, pages 29-33, Schloss Hagenberg by Linz (Austria), oct 1997. RISC-Linz Report Series No. 97-50.<\/li>\n<li>Thierry Boy de la Tour. Ground resolution with group computations on semantic symmetries. In <em>Proceedings of the 13th Conference on Automated Deduction CADE-13<\/em>, Lecture Notes in Artificial Intelligence 1104, pages 478-492. Springer Verlag, 1996.<\/li>\n<li>Thierry Boy de la Tour and Stephane Demri. On the complexity of extending ground resolution with symmetry rules. In <em>Proceedings of the International Joint Conference on Artificial Intelligence IJCAI&#8217;95<\/em>, pages 289-295. Morgan Kaufmann, 1995.<\/li>\n<li>Thierry Boy de la Tour. An optimality result for clause form translation. <em>Journal of Symbolic Computation<\/em>, 14:283-301, 1992.<\/li>\n<li>Thierry Boy de la Tour and Christoph Kreitz. Building proofs by analogy via the curry-howard isomorphism. In A. Voronkov, editor, <em>Proceedings of the Conference on Logic Programming and Automated Reasoning LPAR&#8217;92<\/em>, Lecture Notes in Artificial Intelligence 624, pages 202-213. Springer Verlag, 1992.<\/li>\n<li>Thierry Boy de la Tour. <em>Optimisations par renommage dans la m\u00e9thode de r\u00e9solution<\/em>. PhD thesis, Institut National Polytechnique de Grenoble, January 1991.<\/li>\n<li>Thierry Boy de la Tour. Minimizing the number of clauses by renaming. In Mark E. Stickel, editor, <em>Proceedings of the 10th International Conference on Automated Deduction CADE-10<\/em>, Lecture Notes in Artificial Intelligence 449, pages 558-572. Springer Verlag, July 1990.<\/li>\n<li>Thierry Boy de la Tour and Gilles Chaminade. Renommage et forme clausale. In <em>Actes des 3emes Journ\u00e9es nationales PRC-GDR Intelligence artificielle<\/em>, pages 183-192. \u00e9ditions Herm\u00e8s, March 1990.<\/li>\n<li>Thierry Boy de la Tour and Gilles Chaminade. The use of renaming to improve the efficiency of clausal theorem proving. In P. Jorrand and V. Sgurev, editors, <em>AIMSA&#8217;90, Artificial Intelligence&#8211;Methodology Systems Application<\/em>. North-Holland, 1990.<\/li>\n<li>Thierry Boy de la Tour. A locally optimal transformation into clause form using partial formula renaming. Rr 765-i-imag &#8211; 90 lifia, institut IMAG, BP 68, 38402 Saint Martin d&#8217;H\u00e8res cedex, January 1989.<\/li>\n<li>Thierry Boy de la Tour, Ricardo Caferra, and Gilles Chaminade. Some tools for an inference laboratory (atinf). In E. Lusk and R. Overbeek, editors, <em>Proccedings of the 9th International Conference on Automated Deduction CADE-9<\/em>, Lecture Notes in Computer Science 310, pages 744-745. Springer Verlag, 1988.<\/li>\n<li>Thierry Boy de la Tour, Ricardo Caferra, and Gilles Chaminade. Towards an inference laboratory. In P. Lorents, G. Mints, and E. Tyugu, editors, <em>Proceedings of the International Conference in Computer Logic, part II<\/em>, pages 5-13. Institute of Cybernetics at the Academy of Sciences of the Estonian SSR, 1988.<\/li>\n<li>Thierry Boy de la Tour, Ricardo Caferra, and Gilles Chaminade. Some tools for an inference laboratory atinf. In <em>Symposium on Theoretical Aspects of Computer Science STACS-88<\/em>, Lecture Notes in Computer Science 294, pages 395-396. Springer Verlag, 1988.<\/li>\n<li>Thierry Boy de la Tour and Ricardo Caferra. A formal approach to some usually informal techniques used in mathematical reasoning. In P. Gianni, editor, <em>Proceedings of the International Symposium on Symbolic and Algebraic Computation ISSAC-88<\/em>, Lecture Notes in Computer Science 358, pages 402-406. Springer Verlag, 1988.<\/li>\n<li>Thierry Boy de la Tour and Ricardo Caferra. L&#8217;analogie en d\u00e9monstration automatique: une approche de la g\u00e9n\u00e9ralisation utilisant le filtrage du second ordre. In <em>Actes du Sixi\u00e8me Congr\u00e8s en Reconnaissance des Formes et Intelligence Artificielle, tome 2<\/em>, pages 809-818. Dunod Informatique, 1987.<\/li>\n<li>Thierry Boy de la Tour and Ricardo Caferra. Proof analogy in interactive theorem proving: A method to express and use it via second order matching. In <em>Proceedings of the Sixth National Conference on Artificial Intelligence AAAI-87<\/em>, pages 95-99. Morgan Kaufmann, 1987.<\/li>\n<\/ul>\n<div id=\"ir-ext-ui\" style=\"color: #000000; font-size: 16px; line-height: 16px; background-color: #f7f7f7; border: 1px solid #999999; border-radius: 1px; top: 1px; left: 1px;\">\n<div class=\"ir-ext-dimensions\"><span class=\"ir-ext-rendered\" title=\"Rendered image dimensions (after any scaling\/resizing has been applied)\"> x <\/span> <span class=\"ir-ext-natural\" title=\"Natural image dimensions (without applying any scaling\/resizing)\"> (x) <\/span><\/div>\n<div class=\"ir-ext-filesize\"><\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>(page en construction) &nbsp; Thierry Boy de la Tour and Nicolas Peltier. Proof generalization in LK by second order unifier minimization. Journal of Automated Reasoning, pages 1-36, 2016. published online Thierry Boy de la Tour and Nicolas Peltier. Analogy in automated deduction: A survey. In Henri Prade and Gilles Richard, editors, Computational Approaches to Analogical [&hellip;]<\/p>\n","protected":false},"author":836,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-22","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/pages\/22","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/users\/836"}],"replies":[{"embeddable":true,"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/comments?post=22"}],"version-history":[{"count":4,"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/pages\/22\/revisions"}],"predecessor-version":[{"id":101,"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/pages\/22\/revisions\/101"}],"wp:attachment":[{"href":"https:\/\/lig-membres.imag.fr\/boydelat\/wp-json\/wp\/v2\/media?parent=22"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}