[:fr]Publications[:]

[:fr](page en construction)

 

  • 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 Reasoning: Current Trends, volume 548 of Studies in Computational Intelligence, pages 103-130. Springer, 2014.
  • Thierry Boy de la Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, and Camilla Schwind. Déduction Automatique, volume 2 of Panorama de l’Intelligence Artificielle, chapter 3. Cépaduès, 2014.
  • Thierry Boy de la Tour and Mnacho Echenim. Solving linear constraints in elementary abelian p-groups of symmetries. CoRR, abs/1107.4553, 2011.
  • 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, 4th International Joint Conference, IJCAR 2008, LNAI 5195, pages 332-347, Sydney, Australia, August 2008. Springer Verlag.
  • Thierry Boy de la Tour and Mnacho Echenim. Determining unify-stable presentations. In Franz Baader, editor, 18th International Conference on Rewriting Techniques and Applications, RTA 2007, Lecture Notes In Computer Science 4533, Paris, France, June 2007. Springer Verlag.
  • Thierry Boy de la Tour and Mnacho Echenim. Permutative rewriting and unification. Information and Computation, 25(4):624-650, april 2007.
  • 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, Proceedings of the 5th International Workshop on Strategies in Automated Deduction (Strategies 2004), volume 125 of Electronic Notes in Theoretical Computer Science, pages 91-113. Elsevier, 15 march 2005.
  • Thierry Boy de la Tour and Mnacho Echenim. Unification in a class of permutative theories. In Jürgen Giesl, editor, 16th International Conference on Rewriting Techniques and Applications, RTA 2005, Lecture Notes In Computer Science 3467, pages 105-119, Nara, Japan, april 2005. Springer Verlag.
  • Thierry Boy de la Tour and Mnacho Echenim. On the complexity of deduction modulo leaf permutative equations. Journal of Automated Reasoning, 33(3-4):271-317, October 2004.
  • 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, Fifth Workshop on Strategies in Automated Deduction, pages 41-51, Cork, Ireland, july 2004. University College Cork.
  • Thierry Boy de la Tour and Mnacho Echenim. Overlapping leaf permutative equations. In David Basin and Michaël Rusinowitch, editors, Second International Joint Conference on Automated Reasoning, IJCAR 2004, Lecture Notes In Artificial Intelligence 3097, pages 430-444, Cork, Ireland, july 2004. Springer Verlag.
  • Thierry Boy de la Tour and Mnacho Echenim. Np-completeness results for deductive problems on stratified terms. In Moshe Vardi and Andrei Voronkov, editors, 10th International Conference on Logic Programming and Automated Reasoning LPAR, Lecture Notes In Artificial Intelligence 2850, pages 315-329, Almaty, Kazakhstan, september 2003. Springer Verlag.
  • Thierry Boy de la Tour and Mnacho Echenim. On leaf permutative theories and occurrence permutation groups. In Ingo Dahn and Laurent Vigneron, editors, 4th International Workshop on First-Order Theorem Proving FTP’2003, volume 86 of Electronic Notes in Theoretical Computer Science, Valencia, spain, may 2003. Elsevier.
  • Thierry Boy de la Tour and Mnacho Echenim. On leaf permutative theories and occurrence permutation groups. In Ingo Dahn and Laurent Vigneron, editors, 4th International Workshop on First-Order Theorem Proving FTP’2003, Valencia, spain, june 2003. Technical Report DSIC-II/10/03.
  • Thierry Boy de la Tour. A note on symmetry heuristics in SEM. In Andrei Voronkov, editor, Proceedings of the 18th Conference on Automated Deduction CADE-18, Lecture Notes in Artificial Intelligence 2392, pages 181-194, Copenhagen, Denmark, july 2002. Springer Verlag.
  • Thierry Boy de la Tour. Some techniques of isomorph-free search. In Artificial Intelligence and Symbolic Computation, International Conference AISC’2000, pages 240-252. Springer Verlag, 2000. Lecture Notes in Artificial Intelligence 1930.
  • Thierry Boy de la Tour. On the complexity of finite sorted algebras. In Ricardo Caferra and Gernot Salzer, editors, Automated Deduction in Classical and Non-Classical Logics, Lecture Notes in Artificial Intelligence 1761, pages 95-108. Springer Verlag, 2000.
  • Thierry Boy de la Tour, Stéphane Févre, and Dongming Wang. Clifford term rewriting for geometric reasoning in 3d. In Xiaoshan Gao, Dongming Wang, and Lu Yang, editors, Automated Deduction in Geometry (ADG’98), Lecture Notes in Artificial Intelligence 1669, pages 130-155. Springer Verlag, 1999.
  • Thierry Boy de la Tour. How complex is a finite first-order sorted interpretation? In Ricardo Caferra and Gernot Salzer, editors, FTP’98 International Workshop on First-Order Theorem Proving, pages 76-85, Vienne, Autriche, nov 1998. Technical Report E1852-GS-981 TU Wien.
  • Thierry Boy de la Tour. Up-to-isomorphism enumeration of finite models – the monadic case. In Maria Paola Bonacina and Ulrich Furbach, editors, FTP97 International Workshop First-Order Theorem Proving, pages 29-33, Schloss Hagenberg by Linz (Austria), oct 1997. RISC-Linz Report Series No. 97-50.
  • Thierry Boy de la Tour. Ground resolution with group computations on semantic symmetries. In Proceedings of the 13th Conference on Automated Deduction CADE-13, Lecture Notes in Artificial Intelligence 1104, pages 478-492. Springer Verlag, 1996.
  • Thierry Boy de la Tour and Stephane Demri. On the complexity of extending ground resolution with symmetry rules. In Proceedings of the International Joint Conference on Artificial Intelligence IJCAI’95, pages 289-295. Morgan Kaufmann, 1995.
  • Thierry Boy de la Tour. An optimality result for clause form translation. Journal of Symbolic Computation, 14:283-301, 1992.
  • Thierry Boy de la Tour and Christoph Kreitz. Building proofs by analogy via the curry-howard isomorphism. In A. Voronkov, editor, Proceedings of the Conference on Logic Programming and Automated Reasoning LPAR’92, Lecture Notes in Artificial Intelligence 624, pages 202-213. Springer Verlag, 1992.
  • Thierry Boy de la Tour. Optimisations par renommage dans la méthode de résolution. PhD thesis, Institut National Polytechnique de Grenoble, January 1991.
  • Thierry Boy de la Tour. Minimizing the number of clauses by renaming. In Mark E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction CADE-10, Lecture Notes in Artificial Intelligence 449, pages 558-572. Springer Verlag, July 1990.
  • Thierry Boy de la Tour and Gilles Chaminade. Renommage et forme clausale. In Actes des 3emes Journées nationales PRC-GDR Intelligence artificielle, pages 183-192. éditions Hermès, March 1990.
  • 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, AIMSA’90, Artificial Intelligence–Methodology Systems Application. North-Holland, 1990.
  • Thierry Boy de la Tour. A locally optimal transformation into clause form using partial formula renaming. Rr 765-i-imag – 90 lifia, institut IMAG, BP 68, 38402 Saint Martin d’Hères cedex, January 1989.
  • Thierry Boy de la Tour, Ricardo Caferra, and Gilles Chaminade. Some tools for an inference laboratory (atinf). In E. Lusk and R. Overbeek, editors, Proccedings of the 9th International Conference on Automated Deduction CADE-9, Lecture Notes in Computer Science 310, pages 744-745. Springer Verlag, 1988.
  • Thierry Boy de la Tour, Ricardo Caferra, and Gilles Chaminade. Towards an inference laboratory. In P. Lorents, G. Mints, and E. Tyugu, editors, Proceedings of the International Conference in Computer Logic, part II, pages 5-13. Institute of Cybernetics at the Academy of Sciences of the Estonian SSR, 1988.
  • Thierry Boy de la Tour, Ricardo Caferra, and Gilles Chaminade. Some tools for an inference laboratory atinf. In Symposium on Theoretical Aspects of Computer Science STACS-88, Lecture Notes in Computer Science 294, pages 395-396. Springer Verlag, 1988.
  • Thierry Boy de la Tour and Ricardo Caferra. A formal approach to some usually informal techniques used in mathematical reasoning. In P. Gianni, editor, Proceedings of the International Symposium on Symbolic and Algebraic Computation ISSAC-88, Lecture Notes in Computer Science 358, pages 402-406. Springer Verlag, 1988.
  • Thierry Boy de la Tour and Ricardo Caferra. L’analogie en démonstration automatique: une approche de la généralisation utilisant le filtrage du second ordre. In Actes du Sixième Congrès en Reconnaissance des Formes et Intelligence Artificielle, tome 2, pages 809-818. Dunod Informatique, 1987.
  • 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 Proceedings of the Sixth National Conference on Artificial Intelligence AAAI-87, pages 95-99. Morgan Kaufmann, 1987.

[:]