Skip to main content
SpringerLink
Log in

Herbrand Theorems for Substructural Logics

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8312))

Abstract

Herbrand and Skolemization theorems are obtained for a broad family of first-order substructural logics. These logics typically lack equivalent prenex forms, a deduction theorem, and reductions of semantic consequence to satisfiability. The Herbrand and Skolemization theorems therefore take various forms, applying either to the left or right of the consequence relation, and to restricted classes of formulas.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Baaz, M., Ciabattoni, A., Fermüller, C.: Herbrand theorem for prenex Gödel logic and its consequences for theorem proving. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 201–216. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  2. Baaz, M., Iemhoff, R.: On Skolemization in constructive theories. Journal of Symbolic Logic 73(3), 969–998 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  3. Baaz, M., Metcalfe, G.: Herbrand Theorems and Skolemization for Prenex Fuzzy Logics. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 22–31. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Baaz, M., Metcalfe, G.: Herbrand’s theorem, Skolemization, and proof systems for first-order Łukasiewicz logic. Journal of Logic and Computation 20(1), 35–54 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  5. Buss, S. (ed.): Handbook of Proof Theory. Kluwer (1998)

    Google Scholar 

  6. Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory for substructural logics: Cut-elimination and completions. Annals of Pure and Applied Logic 163(3), 266–290 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cintula, P., Hájek, P., Noguera, C. (eds.): Handbook of Mathematical Fuzzy Logic (in 2 volumes). College Publications, London (2011)

    Google Scholar 

  8. Cintula, P., Noguera, C.: A general framework for mathematical fuzzy logic. In: Cintula, P., Hájek, P., Noguera, C. (eds.) Handbook of Mathematical Fuzzy Logic, vol. 1, pp. 103–207. College Publications (2011)

    Google Scholar 

  9. Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Studies in Logic and the Foundations of Mathematics, vol. 151. Elsevier, Amsterdam (2007)

    Google Scholar 

  10. García-Cerdaña, À., Armengol, E., Esteva, F.: Fuzzy description logics and t-norm based fuzzy logics. International Journal of Approximate Reasoning 51(6), 632–655 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  11. Hájek, P.: Metamathematics of Fuzzy Logic. Trends in Logic, vol. 4. Kluwer, Dordrecht (1998)

    Google Scholar 

  12. Hájek, P.: Making fuzzy description logic more general. Fuzzy Sets and Systems 154(1), 1–15 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  13. McNaughton, R.: A theorem about infinite-valued sentential logic. Journal of Symbolic Logic 16(1), 1–13 (1951)

    Article  MathSciNet  MATH  Google Scholar 

  14. Meghini, C., Sebastiani, F., Straccia, U.: A model of multimedia information retrieval. Journal of the ACM 48(5), 909–970 (2001)

    Article  MathSciNet  Google Scholar 

  15. Metcalfe, G., Olivetti, N., Gabbay, D.M.: Proof Theory for Fuzzy Logics. Applied Logic Series, vol. 36. Springer (2008)

    Google Scholar 

  16. Minc, G.E.: The Skolem method in intuitionistic calculi. Proceedings of the Steklov Institute of Mathematics 121, 73–109 (1974)

    MathSciNet  MATH  Google Scholar 

  17. Ono, H.: Algebraic semantics for predicate logics and their completeness. In: Orlowska, E. (ed.) Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa, pp. 637–650. Physica Verlag, Heidelberg (1999)

    Google Scholar 

  18. Ono, H.: Crawley completions of residuated lattices and algebraic completeness of substructural predicate logics. Studia Logica 100(1-2), 339–359 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  19. Restall, G.: An Introduction to Substructural Logics. Routledge, New York (2000)

    Google Scholar 

  20. Terui, K.: Herbrand’s theorem via hypercanonical extensions (manuscript)

    Google Scholar 

  21. Vojtáš, P.: Fuzzy logic programming. Fuzzy Sets and Systems 124(3), 361–370 (2001)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Academy of Sciences, Prague, Czech Republic

    Petr Cintula

  2. Mathematical Institute, University of Bern, Switzerland

    George Metcalfe

Authors
  1. Petr Cintula
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. George Metcalfe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Ken McMillan

  2. University of Innsbruck, Austria

    Aart Middeldorp

  3. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cintula, P., Metcalfe, G. (2013). Herbrand Theorems for Substructural Logics. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_39

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-45221-5_39

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-45220-8

  • Online ISBN: 978-3-642-45221-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation