[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Theorem proving systems of the Formel project

  • Extended Abstracts Of Current Deduction Systems
  • Conference paper
  • First Online:
8th International Conference on Automated Deduction (CADE 1986)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 230))

Included in the following conference series:

  • 156 Accesses

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. “The ML Handbook, Version 6.1.” Internal document, Projet Formel, Inria (July 1985).

    Google Scholar 

  2. Th. Coquand. “Une théorie des constructions.” Thèse de troisième cycle, Université Paris VII (Jan. 85).

    Google Scholar 

  3. Th. Coquand. “An analysis of Girard's paradox.” First Conference on Logic in Computer Science, Boston (June 1986).

    Google Scholar 

  4. Th. Coquand, G. Huet. “A Theory of Constructions.” Preliminary version, presented at the International Symposium on Semantics of Data Types, Sophia-Antipolis (June 84).

    Google Scholar 

  5. Th. Coquand, G. Huet. “Constructions: A Higher Order Proof System for Mechanizing Mathematics.” EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985).

    Google Scholar 

  6. Th. Coquand, G. Huet. “Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions.” Colloque de Logique, Orsay (Juil. 1985). To appear, North-Holland.

    Google Scholar 

  7. Th. Coquand, G. Huet. “The Calculus of Constructions.” To appear, JCSS (1986).

    Google Scholar 

  8. F. Fages. “Formes canoniques dans les algèbres booléennes et application à la démonstration automatique en logique de premier ordre.” Thèse de 3ème cycle, Univ. de Paris VI (Juin 1983).

    Google Scholar 

  9. F. Fages. “Le système KB: présentation et bibliographie, mise en œuvre.” Rapport Interne Inria (1984).

    Google Scholar 

  10. G. Huet, J.M. Hullot. “Proofs by Induction in Equational Theories With Constructors.” JCSS 25,2 (1982) 239–266.

    Google Scholar 

  11. J.M. Hullot “Compilation de Formes Canoniques dans les Théories Equationnelles.” Thèse de 3ème cycle, U. de Paris Sud (Nov. 80).

    Google Scholar 

  12. Ph. Le Chenadec. “Le système Al-Zebra pour algèbres finiment présentées, manuel de référence.” Rapport Technique, Greco de Programmation (1985).

    Google Scholar 

  13. Ph. Le Chenadec. “Canonical forms in finitely presented algebras”. Lecture Notes in Theoretical Computer Science, Pitman-Wiley (1986).

    Google Scholar 

  14. C. Mohring. “Algorithm Development in the Calculus of Constructions.” IEEE Symposium on Logic in Computer Science, Cambridge, Mass. (June 1986).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Domaine de Voluceau, INRIA, 78150, Rocquencourt, France

    Gérard Huet

Authors
  1. Gérard Huet
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jörg H. Siekmann

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huet, G. (1986). Theorem proving systems of the Formel project. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_138

Download citation

  • DOI: https://doi.org/10.1007/3-540-16780-3_138

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16780-8

  • Online ISBN: 978-3-540-39861-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation