Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Automated Reasoning

IJCAR 2012: Automated Reasoning pp 301–315Cite as

BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics

  • Conference paper

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

Abstract

We give Binary Decision Diagram (BDD) based methods for deciding validity and satisfiability of propositional Intuitionistic Logic  Int and Bi-intuitionistic Tense Logic BiKt. We handle intuitionistic implication and bi-intuitionistic exclusion by treating them as modalities, but the move to an intuitionistic basis requires careful analysis for handling the reflexivity, transitivity and antisymmetry of the underlying Kripke relation. BiKt requires a further extension to handle the interactions between the intuitionistic and modal binary relations, and their converses. We explain our methodology for using the Kripke semantics of these logics to constrain the underlying least and greatest fixpoint approaches of the finite model construction. With some optimisations this technique is competitive with the state of the art theorem provers for Intuitionistic Logic using the ILTP benchmark and randomly generated formulae.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Avellone, A., Fiorino, G., Moscato, U.: Optimization techniques for propositional intuitionistic logic and their implementation. Theoretical Computer Science 409(1), 41–58 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003)

    Google Scholar 

  3. Buddy (2011), http://sourceforge.net/projects/buddy/

  4. Buisman, L., Goré, R.: A Cut-Free Sequent Calculus for Bi-intuitionistic Logic. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol. 4548, pp. 90–106. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Goré, R., Thomson, J., Widmann, F.: An experimental comparison of theorem provers for CTL. In: TIME 2011: Eighteenth International Symposium on Temporal Representation and Reasoning, pp. 49–56 (September 2011)

    Google Scholar 

  6. Goré, R., Postniece, L., Tiu, A.: Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In: AiML 2008, pp. 43–66 (2008)

    Google Scholar 

  7. Goré, R., Postniece, L., Tiu, A.: Cut-elimination and proof search for bi-intuitionistic tense logic. In: Advances in Modal Logic, pp. 156–177 (2010)

    Google Scholar 

  8. Goré, R., Widmann, F.: Sound Global State Caching for ALC with Inverse Roles. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 205–219. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Marrero, W.: Using BDDs to Decide CTL. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 222–236. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. McLaughlin, S., Pfenning, F.: The focused constraint inverse method for intuitionistic modal logics (2010), (unpublished manuscript) (accessed January 31, 2012)

    Google Scholar 

  11. McLaughlin, S., Pfenning, F.: Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 174–181. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for the modal logic K. Journal of Applied Non-classical Logics 49 (2005)

    Google Scholar 

  13. Pinto, L., Uustalu, T.: Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 295–309. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Postniece, L.: Deep Inference in Bi-intuitionistic Logic. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds.) WoLLIC 2009. LNCS, vol. 5514, pp. 320–334. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Postniece, L.: Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic. Ph.D. thesis, Australian National University (2011)

    Google Scholar 

  16. Raths, T., Otten, J.: The ILTP library (2007), http://www.cs.uni-potsdam.de/ti/iltp/ (accessed January 2012)

  17. Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic, release v1.1. Journal of Automated Reasoning (2006)

    Google Scholar 

  18. Rauszer, C.: Applications of Kripke models to Heyting-Brouwer logic. Studia Logica 36, 61–71 (1977)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Logic and Computation Group, Research School of Computer Science, The Australian National University, Australia

    Rajeev Goré & Jimmy Thomson

Authors
  1. Rajeev Goré
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jimmy Thomson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9, E185/2, 1040, Wien, Austria

    Bernhard Gramlich

  2. École Polytechnique, INRIA Saclay and Laboratoire d’Informatique, Route de Saclay, 91128, Palaiseau Cedex, France

    Dale Miller

  3. School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Uli Sattler

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goré, R., Thomson, J. (2012). BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31365-3_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31364-6

  • Online ISBN: 978-3-642-31365-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation