In this work 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 E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of leanTAP and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having a sequent with an empty left-hand side and containing only that formula on the right-hand side as a root, 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.
AlendaR., OlivettiN., Pozzato.G.L.. CSLlean: A theorem-prover for the logic of comparative concept similarity, Electronic Notes in Theoretical Computer Science (ENTCS)262(3) (2010), 16.
2.
AskounisD., KoutrasC.D., Zikos.Y.. Knowledge means ‘all’, belief means ‘most’, Journal of Applied Non-Classical Logics26(3) (2016), 173–192.
3.
Chellas.B.F., Modal Logic, Cambridge University Press, (1980).
4.
DalmonteT., NegriS., OlivettiN., Pozzato.G.L.. PRONOM: proof-search and countermodel generation for non-normal modal logics. In Mario Alviano, Gianluigi Greco, and Francesco Scarcello, editors, AI*IA 2019 –
Advances in Artificial Intelligence - XVIIIth International
Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19-22, 2019, Proceedings, volume 11946 of Lecture Notes in Computer Science, pages 165–179. Springer, (2019).
5.
DalmonteT., OlivettiN., Negri.S.. Nonnormal modal logics: Bi-neighbourhood semantics and its labelled calculi, In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe, and Thomas Studer, editors, Advances
in Modal Logic 12, proceedings of the 12th conference
on Advances in Modal Logic, held in Bern, Switzerland,
August 27–31, 2018, pages 159–178. College Publications,
(2018).
6.
GiordanoL., GliozziV., OlivettiN., Pozzato.G.L.. Analytic tableaux for KLM preferential and cumulative logics. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic
for Programming, Artificial Intelligence, and Reasoning,
12th International Conference, LPAR 2005, Montego Bay,
Jamaica, December 2–6, 2005, Proceedings, volume 3835
of Lecture Notes in Computer Science, pages 666–681.
Springer, (2005).
7.
GiordanoL., GliozziV., Pozzato.G.L.. KLMLean 2.0: A theorem prover for KLM logics of nonmonotonic reasoning. In Nicola Olivetti, editor, Automated Reasoning
with Analytic Tableaux and Related Methods – Proceedings
of TABLEAUX2007 (16th International Conference on
Automated Reasoning with Analytic Tableaux and Related
Methods), volume 4548 of Lecture Notes in Artificial Intelligence
LNAI, pages 238–244, Aix en Provence, France,
July (2007). Springer.
8.
GirlandoM., LellmannB., OlivettiN., PozzatoG.L., VitalisQ.. VINTE: An implementation of internal calculi for lewis logics of counterfactual reasoning. In Claudia Nalon and Renate Schmidt, editors, Proceedings
of TABLEAUX 2017 - 26th International Conference on
Automated Reasoning with Analytic Tableaux and Related
Methods, volume 10501 of Lecture Notes in Artificial Intelligence
LNAI, pages 149 – 159, Brasilia, Brazil, September
(2017). Springer.
9.
GiunchigliaE., TacchellaA., Giunchiglia.F.. Sat-based decision procedures for classical modal logics, Journal of Automated Reasoning28(2) (2002), 143–171.
10.
HansenH.. Tableau games for coalition logic and alternating-time temporal logic–theory and implementation, Master’s thesis, University of Amsterdam (2004).
11.
LavendhommeR., Lucas.T.. Sequent calculi and decision procedures for weak modal systems, Studia Logica65 (2000), 121–145.
12.
Lellmann.B.. Countermodels for non-normal modal logics via nested sequents. In Nick Bezhanishvili and Yde Venema, editors, SYSMICS2019 - Booklet of Abstracts, pages
107–110. Institute for Logic, Language and Computation
University of Amsterdam, (2019).
13.
Negri.S.. Proof analysis in modal logic, J. Philosophical Logic34(5-6) (2005), 507–544.
14.
Negri.S.. Proof theory for non-normal modal logics: The neighbourhood formalism and basic results, IfCoLog J. Log. Appl4(4) (2017), 1241–1286.
15.
OlivettiN., Pozzato.G.L.. CondLean: A theorem prover for conditional logics. In Marta Cialdea Mayer and Fiora Pirri, editors, Automated Reasoning with Analytic Tableaux
and Related Methods - Proceedings of TABLEAUX 2003
(12th International Conference on Automated Reasoning
with Analytic Tableaux and Related Methods), volume
2796 of Lecture Notes in Artificial Intelligence LNAI, pages
264 – 270, Roma, Italy, September (2003). Springer.
16.
OlivettiN., Pozzato.G.L.. CondLean 3.0: Improving Condlean for stronger conditional logics. In hard Beckert, editor, Automated Reasoning with Analytic
Tableaux and Related Methods - Proceedings of
TABLEAUX 2005 (14th International Conference on Automated
Reasoning with Analytic Tableaux and Related
Methods), volume 3702 of Lecture Notes in Artificial
Intelligence LNAI, pages 328 – 332, Koblenz, Germany,
September (2005). Springer.
17.
OlivettiN., Pozzato.G.L.. Theorem proving for conditional logics: CondLean and GoalDuck, Journal of Applied Non-Classical Logics18 (2008), 427–473.
18.
OlivettiN., Pozzato.G.L.. NESCOND: an implementation of nested sequent calculi for conditional logics. In Stephane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Proceedings of IJCAR 2014 (7th
International Joint Conference on Automated Reasoning),
volume 8562 of Lecture Notes in Artificial Intelligence
LNAI, pages 511–518, Vienna (Austria), July (2014).
Springer.
19.
OlivettiN., Pozzato.G.L.. Nested sequent calculi and theorem proving for normal conditional logics: The theorem prover NESCOND, Intelligenza Artificiale9 (2015), 109–125.
20.
Pacuit.E.. Neighborhood semantics for modal logic. Springer, (2017).
21.
PaulyM.. A modal logic for coalitional power in games, Journal of Logic and Computation12(1) (2002), 149–166.
22.
RossA.. Imperatives and logic, Theoria7 (1941), 53–71.
23.
VardiM.Y.. On epistemic logic and logical omniscience, In Theoretical aspects of reasoning about knowledge, pages 293–305, Elsevier, (1986).
