Skip to main content
SpringerLink
Log in

First-Order Logic with Dependent Types

  • Conference paper
Automated Reasoning (IJCAR 2006)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4130))

Included in the following conference series:

Abstract

We present DFOL, an extension of classical first-order logic with dependent types, i.e., as in Martin-Löf type theory, signatures may contain type-valued function symbols. A model theory for the logic is given that stays close to the established first-order model theory. The logic is presented as an institution, and the logical framework LF is used to define signatures, terms and formulas. We show that free models over Horn theories exist, which facilitates its use as an algebraic specification language, and show that the classical first-order axiomatization is complete for DFOL, too, which implies that existing first-order theorem provers can be extended. In particular, the axiomatization can be encoded in LF.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bertot, Y., Castéran, P.: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  2. Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. Bidoit, M., Mosses, P.D. (eds.): CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  4. Constable, R., Allen, S., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J., Smith, S.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs (1986)

    Google Scholar 

  5. Cartmell, J.: Generalized algebraic theories and contextual category. Annals of Pure and Applied Logic 32 (1986)

    Google Scholar 

  6. Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic, vol. 4, pp. 65–89 (1996)

    Google Scholar 

  7. Diaconescu, R.: Institution-independent Model Theory (2005)

    Google Scholar 

  8. Dybjer, P.: Internal type theory. In: TYPES, pp. 120–134 (1995)

    Google Scholar 

  9. Gallier, J.: Foundations of Automatic Theorem Proving. Wiley, Chichester (1986)

    MATH  Google Scholar 

  10. Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)

    MATH  MathSciNet  Google Scholar 

  11. Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.: Introducing OBJ. In: Goguen, J. (ed.) Applications of Algebraic Specification using OBJ, Cambridge (1993)

    Google Scholar 

  12. Henkin, L.: The completeness of the first-order functional calculus. Journal of Symbolic Logic 14, 159–166 (1949)

    Article  MATH  MathSciNet  Google Scholar 

  13. Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: CSL, pp. 427–441 (1994)

    Google Scholar 

  14. Huet, G., Saïbi, A.: Constructive category theory. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner., MIT Press, Cambridge (1998)

    Google Scholar 

  15. Harper, R., Sannella, D., Tarlecki, A.: Structured presentations and logic representations. Annals of Pure and Applied Logic 67, 113–160 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  16. Makkai, M.: First order logic with dependent sorts (FOLDS) (Unpublished)

    Google Scholar 

  17. Martin-Löf, P.: An intuitionistic theory of types: Predicative part. In: Proceedings of the 1973 Logic Colloquium, North-Holland, Amsterdam (1974)

    Google Scholar 

  18. Nieuwenhuis, R., Rubio, A.: Paramodulation-Based theorem proving. In: Handbook of Automated Reasoning, pp. 371–443. Elsevier Science Publishers, Amsterdam (2001)

    Chapter  Google Scholar 

  19. Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

  20. Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report SRI-CSL-97-2, SRI International (1997)

    Google Scholar 

  21. Pfenning, F.: Logical frameworks. In: Handbook of automated reasoning, pp. 1063–1147. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  22. Pientka, B., Pfenning, F.: Optimizing higher-order pattern unification. In: 19th International Conference on Automated Deduction, pp. 473–487. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  23. Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  24. Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications 15, 91–110 (2002)

    MATH  Google Scholar 

  25. Seely, R.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95, 33–48 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  26. Schürmann, C., Pfenning, F.: Automated theorem proving in a simple meta-logic for LF. In: Kirchner, C., Kirchner, H. (eds.) Proceedings of the 15th International Conference on Automated Deduction, pp. 286–300. Springer, Heidelberg (1996)

    Google Scholar 

  27. Tarlecki, A.: On the existence of free models in abstract algebraic institutions. Theoretical Computer Science 37, 269–301 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  28. Virga, R.: Higher-order superposition for dependent types. In: Ganzinger, H. (ed.) Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pp. 123–137. Springer, Heidelberg (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University and International University Bremen,  

    Florian Rabe

Authors
  1. Florian Rabe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Artificial Intelligence Research Group, University of Koblenz-Landau, Universitätsstr. 1, 56070, Koblenz

    Ulrich Furbach

  2. SRI International, MS EL256,, 333 Ravenswood Avenue, 94025-3493, Menlo Park, CA, USA

    Natarajan Shankar

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rabe, F. (2006). First-Order Logic with Dependent Types. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814771_33

Download citation

  • DOI: https://doi.org/10.1007/11814771_33

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation