Invited Talk: Coherentisation of First-Order Logic | SpringerLink
Skip to main content
Springer Nature Link
Log in

Invited Talk: Coherentisation of First-Order Logic

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015)

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

  • 520 Accesses

Abstract

This talk explores the relationship between coherent (aka “geometric”) logic and first-order logic FOL, with special reference to the coherence/geometricity required of accessibility conditions in Negri’s work on modal logic (and our work with her on intermediate logic). It has been known to some since the 1970s that every first-order theory has a coherent conservative extension, and weaker versions of this result have been used in association with the automation of coherent logic; but, it is hard to find the result in the literature. We discuss various proofs of the result, and present a coherentisation algorithm with the desirable property of being idempotent. An announcement was in [7]; details can be found in [8].

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

References

  1. Antonius, W.: Théories cohérentes et prétopos, Thèse de Maitrise, Université de Montréal (1975)

    Google Scholar 

  2. Berghofer, S.: Implementation of a coherent logic prover for Isabelle. In: ACL 2008 Workshop (2008), http://wwwbroy.in.tum.de/~berghofe/papers/ACL08_slides.pdf

  3. Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 246–260. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Bezem, M., Hendricks, D.: On the mechanization of the proof of Hessenberg’s Theorem in coherent logic. J. Autom. Reasoning 40, 61–85 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bourhis, P., Morak, M., Pieris, A.: Towards efficient reasoning under guarded-based disjunctive existential rules. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 99–110. Springer, Heidelberg (2014)

    Google Scholar 

  6. Dyckhoff, R., Negri, S.: Proof analysis in intermediate logics. Arch. for Math. Logic 51, 71–92 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  7. Dyckhoff, R., Negri, S.: Coherentisation of accessibility conditions in labelled sequent calculi. In: GSB Workshop, Vienna Summer of Logic (2014)

    Google Scholar 

  8. Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symbol. Logic 21, 123–163 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  9. Fisher, J., Bezem, M.: Skolem machines. Fundamenta Informaticae 91, 79–103 (2009)

    MathSciNet  MATH  Google Scholar 

  10. Gogacz, T., Marcinkowski, J.: All–Instances termination of Chase is undecidable. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 293–304. Springer, Heidelberg (2014)

    Google Scholar 

  11. Holen, B., Hovland, D., Giese, M.: Efficient rule-matching for hyper-tableaux. In: Proc. 9th International Workshop on Implementation of Logics, EasyChair Proceedings in Computing Series, vol. 22, pp. 4–17. Easychair (2013)

    Google Scholar 

  12. Johnstone, P.T.: Sketches of an elephant, a topos theory compendium: I and II. Oxford Logic Guides, vols. 43, 44. OUP (2002)

    Google Scholar 

  13. Negri, S.: Proof analysis in modal logic. J. Philos. Logic 34, 507–544 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  14. Negri, S.: Proof analysis beyond geometric theories: from rule systems to systems of rules. J. Logic & Computation (2014), http://logcom.oxfordjournals.org/content/early/2014/06/13/logcom.exu037

  15. de Nivelle, H., Meng, J.: Geometric resolution: A proof procedure based on finite model search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 303–317. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Polonsky, A.: Proofs, types, and lambda calculus. PhD thesis, Univ. Bergen (2010)

    Google Scholar 

  17. Stojanović, S., Pavlović, V., Janičić, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS, vol. 6877, pp. 201–220. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  18. Skolem, T.: Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theorem über dichte Mengen. Skrifter I, vol. 4, pp. 1–36. Det Norske Videnskaps-Akademi (1920)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of St Andrews, St Andrews, UK

    Roy Dyckhoff

Authors
  1. Roy Dyckhoff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roy Dyckhoff .

Editor information

Editors and Affiliations

  1. Uniwersytet Wrocławski, Wrocław, Poland

    Hans De Nivelle

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Dyckhoff, R. (2015). Invited Talk: Coherentisation of First-Order Logic. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24312-2_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24311-5

  • Online ISBN: 978-3-319-24312-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation