VINTE: An Implementation of Internal Calculi for Lewis’ Logics of Counterfactual Reasoning | SpringerLink
Skip to main content
Springer Nature Link
Log in

VINTE: An Implementation of Internal Calculi for Lewis’ Logics of Counterfactual Reasoning

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

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

Abstract

We present VINTE, a theorem prover for conditional logics for counterfactual reasoning introduced by Lewis in the seventies. VINTE implements some internal calculi recently introduced for the basic system \(\mathbb {V}\) and some of its significant extensions with axioms \(\mathbb {N}\), \(\mathbb {T}\), \(\mathbb {C}\), \(\mathbb {W}\) and \(\mathbb {A}\). VINTE is inspired by the methodology of and it is implemented in Prolog. The paper shows some experimental results, witnessing that the performances of VINTE are promising.

Supported by the Project TICAMORE ANR-16-CE91-0002-01, by the EU under Marie Skłodowska-Curie Grant Agreement No. [660047], and by the Project “ExceptionOWL”, Università di Torino and Compagnia di San Paolo, call 2014.

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 7435
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 9294
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

Notes

  1. 1.

    It is worth noticing that in turn the connective \(\preccurlyeq \) can be defined in terms of .

  2. 2.

    Employing this notation, satisfiability of a \( \preccurlyeq \)-formula in a model becomes the following: \(x \Vdash A\preccurlyeq B \) iff for all . \( \alpha \Vdash ^{\forall } \lnot B \) or \( \alpha \Vdash ^{\exists } A \).

  3. 3.

    It is worth noticing that absoluteness can be equally stated as local absoluteness: it holds .

  4. 4.

    It is worth noticing that this translation introduces an exponential blowup.

References

  1. Alenda, R., Olivetti, N., Pozzato, G.L.: Nested sequent calculi for normal conditional logics. J. Log. Comput. 26(1), 7–50 (2016)

    Article  MATH  MathSciNet  Google Scholar 

  2. Baltag, A., Smets, S.: The logic of conditional doxastic actions. Texts Log. Games 4, 9–31 (2008). Special Issue on New Perspectives on Games and Interaction

    MathSciNet  Google Scholar 

  3. Beckert, B., Posegga, J.: leanTAP: lean tableau-based deduction. J. Autom. Reason. 15(3), 339–358 (1995)

    Article  MATH  Google Scholar 

  4. Board, O.: Dynamic interactive epistemology. Games Econ. Behav. 49(1), 49–80 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  5. Genovese, V., Giordano, L., Gliozzi, V., Pozzato, G.L.: Logics in access control: a conditional approach. J. Log. Comput. 24(4), 705–762 (2014)

    Article  MATH  MathSciNet  Google Scholar 

  6. Girlando, M., Lellmann, B., Olivetti, N., Pozzato, G.L.: Standard sequent calculi for Lewis’ logics of counterfactuals. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS, vol. 10021, pp. 272–287. Springer, Cham (2016). doi:10.1007/978-3-319-48758-8_18

    Chapter  Google Scholar 

  7. Girlando, M., Lellmann, B., Olivetti, N., Pozzato, G.L.: Hypersequent calculi for Lewis’ conditional logics with uniformity and reflexivity. In: Nalon, C., Schmidt, R.A. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 131–148. Springer, Cham (2017)

    Google Scholar 

  8. Grahne, G.: Updates and counterfactuals. J. Log. Comput. 8(1), 87–117 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  9. Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1–2), 167–207 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  10. Lewis, D.: Counterfactuals. Blackwell, Hoboken (1973)

    MATH  Google Scholar 

  11. Nute, D.: Topics in Conditional Logic. Reidel, Dordrecht (1980)

    Book  MATH  Google Scholar 

  12. Olivetti, N., Pozzato, G.L.: CondLean 3.0: improving condlean for stronger conditional logics. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 328–332. Springer, Heidelberg (2005). doi:10.1007/11554554_27

    Chapter  Google Scholar 

  13. Olivetti, N., Pozzato, G.L.: Theorem proving for conditional logics: condlean and goalduck. J. Appl. Non-Class. Log. 18(4), 427–473 (2008)

    Article  MATH  Google Scholar 

  14. Olivetti, N., Pozzato, G.L.: NESCOND: an implementation of nested sequent calculi for conditional logics. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 511–518. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_39

    Google Scholar 

  15. Olivetti, N., Pozzato, G.L.: Nested sequent calculi and theorem proving for normal conditional logics: the theorem prover NESCOND. Intelligenza Artificiale 9(2), 109–125 (2015)

    Article  Google Scholar 

  16. Olivetti, N., Pozzato, G.L.: A standard internal calculus for Lewis’ counterfactual logics. In: Nivelle, H. (ed.) TABLEAUX 2015. LNCS, vol. 9323, pp. 270–286. Springer, Cham (2015). doi:10.1007/978-3-319-24312-2_19

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aix Marseille Université, CNRS, ENSAM, Université de Toulon, LSIS UMR 7296, 13397, Marseille, France

    Marianna Girlando & Nicola Olivetti

  2. Technische Universität Wien, Vienna, Austria

    Björn Lellmann

  3. Dipartimento di Informatica, Universitá di Torino, Turin, Italy

    Gian Luca Pozzato

  4. Département Informatique, École Spéciale Militaire de Saint-Cyr, Guer, France

    Quentin Vitalis

Authors
  1. Marianna Girlando
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Björn Lellmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nicola Olivetti
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gian Luca Pozzato
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Quentin Vitalis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marianna Girlando .

Editor information

Editors and Affiliations

  1. University of Manchester, Manchester, United Kingdom

    Renate A. Schmidt

  2. University of Brasília, Brasília D.F., Brazil

    Cláudia Nalon

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Girlando, M., Lellmann, B., Olivetti, N., Pozzato, G.L., Vitalis, Q. (2017). VINTE: An Implementation of Internal Calculi for Lewis’ Logics of Counterfactual Reasoning. In: Schmidt, R., Nalon, C. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2017. Lecture Notes in Computer Science(), vol 10501. Springer, Cham. https://doi.org/10.1007/978-3-319-66902-1_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66902-1_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66901-4

  • Online ISBN: 978-3-319-66902-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation