Researcher identifiers

Number of documents

8

Claude Kirchner


"Thérèse Hardin"   

Journal articles1 document

  • Gilles Dowek, Thérèse Hardin, Claude Kirchner. Theorem Proving Modulo. Journal of Automated Reasoning, Springer Verlag, 2003, 31 (1), pp.33-72. ⟨inria-00099711⟩

Conference papers2 documents

  • Gilles Dowek, Thérèse Hardin, Claude Kirchner. Binding Logic: proofs and models. 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'2002, Oct 2002, Tbilisi, Georgia. pp.130-144. ⟨inria-00101012⟩
  • Gilles Dowek, Thérèse Hardin, Claude Kirchner. HOL-$\lambda \sigma$ an intentional first-order expression of higher-order logic. Tenth International Conference on Rewriting Techniques & Applications - RTA'99, Jul 1999, Trento, Italy, 14 p. ⟨inria-00098847⟩

Reports5 documents

  • Gilles Dowek, Thérèse Hardin, Claude Kirchner. Theorem Proving Modulo Revised Version. [Research Report] RR-4861, INRIA. 2003, pp.54. ⟨inria-00071722⟩
  • Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning. Unification via Explicit Substitutions: The Case of Higher-Order Patterns. [Research Report] RR-3591, INRIA. 1998, pp.33. ⟨inria-00077203⟩
  • Gilles Dowek, Thérèse Hardin, Claude Kirchner. Theorem Proving Modulo. [Research Report] RR-3400, INRIA. 1998, pp.27. ⟨inria-00077199⟩
  • Gilles Dowek, Thérèse Hardin, Claude Kirchner. Holls: an Intentional First-Order Expression of Higher-Order Logic. [Research Report] RR-3556, INRIA. 1998, pp.26. ⟨inria-00077202⟩
  • Gilles Dowek, Thérèse Hardin, Claude Kirchner. Higher Order Unification via Explicit Substitutions. [Research Report] RR-2709, INRIA. 1995, pp.42. ⟨inria-00077197⟩