Some tools for an inference laboratory (ATINF)

  • Thierry Boy de la Tour
  • Ricardo Caferra
  • Gilles Chaminade
Systems Demonstrations
Part of the Lecture Notes in Computer Science book series (LNCS, volume 294)


Theorem Prover Formula Transformer Heuristic Function Automate Deduction Structure Sharing 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [Eder 84]
    E. Eder: "An implementation of a theorem prover based on the connection method". Proc. AIMSA'84. Varna, Bulgaria, September 1984. North-Holland, 121–128.Google Scholar
  2. [Plaisted 86]
    D. Plaisted: "A structure preserving clause form translation". Journal of Symbolic Computation (1986) 2, 293–304.Google Scholar
  3. [Schmidt-Schauss 86]
    M. Schmidt-Schauss: "Unification in many sorted equational theories". Proc. 8th. CADE, Oxford, England, July 1986, 538–552.Google Scholar
  4. [Stickel 85]
    M. Stickel: "Automated deduction by theory resolution". Journal of Automated Reasoning, Vol. 1, No 4, 1985, 333–376.Google Scholar
  5. [Walther 83]
    C. Walther: "A many sorted calculus based on resolution and paramodulation". Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, 882–891.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Thierry Boy de la Tour
    • 1
  • Ricardo Caferra
    • 1
  • Gilles Chaminade
    • 1
  1. 1.LIFIA-INPGGrenoble CedexFrance

Personalised recommendations