Abstract
We present PRONOM, a theorem prover and countermodel generator for non-normal modal logics. PRONOM implements some labelled sequent calculi recently introduced for the basic system \(\mathbf {E}\) and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of
and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having that formula as a root in the labelled calculi, otherwise PRONOM is able to extract a model falsifying it from an open, saturated branch. The paper shows some experimental results, witnessing that the performances of PRONOM are promising.
Supported by the ANR project TICAMORE ANR-16-CE91-0002-01, the Academy of Finland project 1308664 and INdAM project GNCS 2019 “METALLIC #2”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A complete description of the whole cube of NNML will be provided in Sect. 2.
- 2.
As a difference with [4] here terms are multisets rather than sets. This is ininfluent for the properties of the calculi.
- 3.
The user can run PRONOM without using the interface of the web application. To this aim, he just need to invoke the goal prove(f).
References
Alenda, R., Olivetti, N., Pozzato, G.L.: CSL-lean: a theorem-prover for the logic of comparative concept similarity. Electron. Notes Theoret. Comput. Sci. (ENTCS) 262, 3–16 (2010)
Askounis, D., Koutras, C.D., Zikos, Y.: Knowledge means ‘all’, belief means ‘most’. J. Appl. Non-Classical Logics 26(3), 173–192 (2016)
Chellas, B.F.: Modal Logic. Cambridge University Press, Cambridge (1980)
Dalmonte, T., Olivetti, N., Negri, S.: Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi. In: Bezhanishvili, G., D’Agostino, G., Metcalfe, G., Studer, T. (eds.) Advances in Modal Logic 12, Proceedings of the 12th Conference on Advances in Modal Logic, 27–31 August 2018, Held in Bern, Switzerland, pp. 159–178. College Publications (2018)
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). https://doi.org/10.1007/11591191_46
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). https://doi.org/10.1007/978-3-540-73099-6_19
Girlando, M., Lellmann, B., Olivetti, N., Pozzato, G.L., Vitalis, Q.: VINTE: an implementation of internal calculi for Lewis’ logics of counterfactual reasoning. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 149–159. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66902-1_9
Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. J. Automated Reason. 28(2), 143–171 (2002)
Hansen, H.: Tableau games for coalition logic and alternating-time temporal logic-theory and implementation. Master’s thesis, University of Amsterdam (2004)
Lavendhomme, R., Lucas, T.: Sequent calculi and decision procedures for weak modal systems. Studia Logica 65, 121–145 (2000)
Lellmann, B.: Countermodels for non-normal modal logics via nested sequents. In: Bezhanishvili, N., Venema, Y. (eds.) SYSMICS2019 - Booklet of Abstracts, pp. 107–110. Language and Computation University of Amsterdam, Institute for Logic (2019)
Negri, S.: Proof theory for non-normal modal logics: the neighbourhood formalism and basic results. IfCoLog J. Log. Appl. 4(4), 1241–1286 (2017)
Olivetti, N., Pozzato, G.L.: CondLean: a theorem prover for conditional logics. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS (LNAI), vol. 2796, pp. 264–270. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45206-5_23
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). https://doi.org/10.1007/11554554_27
Olivetti, N., Pozzato, G.L.: Theorem proving for conditional logics: CondLean and GoalDuck. J. Appl. Non-Classical Logics 18, 427–473 (2008)
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). https://doi.org/10.1007/978-3-319-08587-6_39
Olivetti, N., Pozzato, G.L.: Nested sequent calculi and theorem proving for normal conditional logics: the theorem prover NESCOND. Intelligenza Artificiale 9, 109–125 (2015)
Pacuit, E.: Neighborhood Semantics for Modal Logic. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-319-67149-9
Pauly, M.: A modal logic for coalitional power in games. J. Logic Comput. 12(1), 149–166 (2002)
Ross, A.: Imperatives and logic. Theoria 7, 53–71 (1941)
Vardi, M.Y.: On epistemic logic and logical omniscience. In: Theoretical Aspects of Reasoning About Knowledge, pp. 293–305. Elsevier (1986)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Dalmonte, T., Negri, S., Olivetti, N., Pozzato, G.L. (2019). PRONOM: Proof-Search and Countermodel Generation for Non-normal Modal Logics. In: Alviano, M., Greco, G., Scarcello, F. (eds) AI*IA 2019 – Advances in Artificial Intelligence. AI*IA 2019. Lecture Notes in Computer Science(), vol 11946. Springer, Cham. https://doi.org/10.1007/978-3-030-35166-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-35166-3_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-35165-6
Online ISBN: 978-3-030-35166-3
eBook Packages: Computer ScienceComputer Science (R0)