Some Computational Aspects of an Order-Sorted Calculus: Order-Sorted Unification Using Compact Representation of Clauses. - Gilles Chaminade (ECAI, 1988)

Some Tools for an Inference Laboratory (ATINF). - Thierry Boy de la Tour; Ricardo Caferra; Gilles Chaminade (STACS, 1988)

The Use of Renaming to Improve the Effeciency of Clausal Theorem Proving. - Thierry Boy de la Tour; Gilles Chaminade (AIMSA, 1990)

Intégration et implémentation de mécanismes de déduction naturelle dans les démonstrateurs utilisant la résolution. (Integration and implementation of natural deduction mechanisms in resolution based theorem provers). - Gilles Chaminade (1991)