An Implementation of a Free-Variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: The Theorem Prover FreeP 1.0 | SpringerLink
Skip to main content

An Implementation of a Free-Variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: The Theorem Prover FreeP 1.0

  • Conference paper
AI*IA 2007: Artificial Intelligence and Human-Oriented Computing (AI*IA 2007)

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

Included in the following conference series:

  • 1621 Accesses

Abstract

We present FreeP 1.0, a theorem prover for the KLM preferential logic P of nonmonotonic reasoning. FreeP 1.0 is a SICStus Prolog implementation of a free-variables, labelled tableau calculus for P, obtained by introducing suitable modalities to interpret conditional assertions. The performances of FreeP 1.0 are promising. FreeP 1.0 can be downloaded at http://www.di.unito.it/~pozzato/FreeP1.0 .

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

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

    Article  MATH  MathSciNet  Google Scholar 

  2. Friedman, N., Halpern, J.Y.: Plausibility measures and default reasoning. Journal of the ACM 48(4), 648–685 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  3. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Analytic Tableaux for KLM Preferential and Cumulative Logics. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 666–681. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Giordano, L., Gliozzi, V., Pozzato, G.L.: KLMLean 2.0: A theorem prover for klm logics of nonmonotonic reasoning. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol. 4548, pp. 238–244. Springer, Heidelberg (2007)

    Google Scholar 

  5. Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. (1996)

    Google Scholar 

  6. Beckert, B., Goré, R.: Free-variable tableaux for propositional modal logics. Studia Logica 69(1), 59–96 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  7. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Analytic Tableaux Calculi for KLM Rational Logic R. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 190–202. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Lehmann, D., Magidor, M.: What does a conditional knowledge base entail? Artificial Intelligence 55(1), 1–60 (1992)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Roberto Basili Maria Teresa Pazienza

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L. (2007). An Implementation of a Free-Variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: The Theorem Prover FreeP 1.0. In: Basili, R., Pazienza, M.T. (eds) AI*IA 2007: Artificial Intelligence and Human-Oriented Computing. AI*IA 2007. Lecture Notes in Computer Science(), vol 4733. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74782-6_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74782-6_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74781-9

  • Online ISBN: 978-3-540-74782-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics