## VINTE

with Marianna Girlando, Björn Lellmann, Nicola Olivetti, Quentin Vitalis

Conditional logics have a long history, and recently they have found several applications in artificial intelligence, such as deductive databases, nonmonotonic reasoning, belief revision. One of the motivating applications was the formalization of counterfactual sentences, conditionals of the form A implies B where A is false. VINTE is a theorem prover implementing internal standard sequent calculi for the conditional logics introduced by Lewis for counterfactual reasoning. It is written in SWI Prolog and can be used by means of a web interface.

For more details, visit VINTE web page

## Related publications:

Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Gian Luca Pozzato, Quentin Vitalis, VINTE: an Implementation of Internal Calculi for Lewis' Logics for Counterfactual Reasoning, In Claudia Nalon and Renate Schmidt, Eds, Proceedings of TABLEAUX 2017 - 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence LNAI 10501, Springer. To appear, 2017.

## NESCOND: an implementation of nested sequent calculi for Conditional Logics

with Nicola Olivetti

Conditional logics have a long history, and recently they have found several applications in artificial intelligence, such as deductive databases, nonmonotonic reasoning, belief revision. NESCOND is a theorem prover implementing nested sequent calculi for these logics. It is written in SWI Prolog and can be used by means of a web interface.

For more details, visit NESCOND web page

## Related publications:

Nicola Olivetti, Gian Luca Pozzato, Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics, In Marianna Nicolosi Asmundo, Domenico Cantone, Eds, Proceedings of CILC 2013, CEUR Workshop Proceedings 1068, pp. 49 - 63, 2013.

Nicola Olivetti, Gian Luca Pozzato, NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics, In Stephane Demri, Deepak Kapur, Christoph Weidenbach, Eds, Proceedings of IJCAR 2014 (7th International Joint Conference on Automated Reasoning), Lecture Notes in Artificial Intelligence LNAI 8562, Springer, pp. 511 - 518, 2014.

## PreDeLo 1.0: a Theorem Prover for Preferential Description Logics

with Laura Giordano, Valentina Gliozzi, Adam Jalal, Nicola Olivetti

Nonmonotonic extensions of Description Logics have been actively investigated since the early 90s. We have introduced a simple but powerful nonmonotonic extension of Description Logics in which typical properties can be directly specified by means of a typicality operator T enriching the underlying DL; the typicality operator T is essentially characterized by the core properties of nonmonotonic reasoning axiomatized by KLM preferential and rational logic. In these logics one can consistently express defeasible inclusions and exceptions such as: typical students do not pay taxes, but working students do typically pay taxes, but working students having children normally do not. PreDeLo 1.0 is a Prolog implementation of labelled tableaux calculi for such extensions, and it is able to deal with the preferential extension of the basic Description Logic ALC as well as with the preferential extension of the lightweight Description Logic DL-Litecore.

For more details, visit PreDeLo web page

## Related publications:

Laura Giordano, Valentina Gliozzi, Adam Jalal, Nicola Olivetti, Gian Luca Pozzato, PreDeLo 1.0: a Theorem Prover for Preferential Description Logics, In Matteo Baldoni, Cristina Baroglio, Guido Boella, Roberto Micalizio, Eds, Proceedings of AI*IA 2013, Lecture Notes in Artificial Intelligence LNAI 8249, Springer, pp. 60 - 72, 2013.

## CSLLean 1.0: a Theorem Prover for the Logic of Comparative Concept Similarity

with Regis Alenda and Nicola Olivetti

The logic CSL of the comparative concept similarity has been introduced by Sheremet, Tishkovsky, Wolterand Zakharyaschev to capture a form of qualitative similarity comparison between concepts and/or objects.In this logic we can formulate assertions of the form "objects A are more similar to B than to C". Thiskind of assertions can be added to an ontology to express qualitative comparisons between concepts. CSLlean 1.0 is the first theorem-prover for this logic. It is a direct Prolog implementation of atableaux-based decision procedure recently proposed for this logic. The Prolog program is inspired by thelean-methodology.

For more details, visit CSLLean web page

## Related publications:

Regis Alenda, Nicola Olivetti, Gian Luca Pozzato, CSL-lean: A theorem-Prover for the logic of Comparative Concept Similarity, Electronic Notes in Theoretical Computer Science (ENTCS) 262, Elsevier, pp. 3 - 16, 2010.

Regis Alenda, Nicola Olivetti, Gian Luca Pozzato, CSL-lean: A theorem-Prover for the logic of Comparative Concept Similarity, In Thomas Bolander, Eds, Proceedings of the 6th International Workshop on Methods for Modalities (M4M-6), 0, pp. 163 - 175, 2009.

## KLMOptimal: an optimal Theorem Prover KLM Preferential logic P

with Laura Giordano, Valentina Gliozzi, Andrea La Spisa, Nicola Olivetti

Kraus, Lehmann and Magidor (KLM) proposed a formalization of non-monotonic reasoning that was early recognized as a landmark. KLMOptimal is a theorem prover implementing an optimal decision procedure for preferential logic P. It is written in SICStus Prolog and it is inspired by the lean methodology.

For more details, visit KLMOptimal web page

## GoalDUCK: a goal-directed theorem prover for Conditional Logics

with Nicola Olivetti

Conditional logics have a long history, and recently they have found several applications in artificial intelligence, such as deductive databases, nonmonotonic reasoning, belief revision. GoalDUCK is a theorem prover implementing a goal-directed proof procedure for the basic system of normal conditional logics CK.

For more details, visit GoalDUCK web page

## Related publications:

Nicola Olivetti, Gian Luca Pozzato, Theorem Proving for Conditional Logics: CondLean and GoalDuck, Journal of Applied Non-Classical Logics 18(4), Taylor & Francis Online, pp. 427 - 473, 2008.

## FreeP 1.0: a Free-Variables Theorem Prover for KLM Preferential Logic P

with Laura Giordano, Valentina Gliozzi, Nicola Olivetti

Kraus, Lehmann and Magidor (KLM) proposed a formalization of non-monotonic reasoning that was early recognized as a landmark. FreeP 1.0 is a theorem prover implementing free-variables tableaux calculi for the Preferential logic P of KLM framework. It is written in SICStus Prolog and also comprises a GUI written in Java.

For more details, visit FreeP web page

## Related publications:

Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, An Impelmentation of a Free-variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning, In Roberto Basili, Maria Teresa Pazienza, Eds, AI*IA 2007: Artificial Intelligence and Human-Oriented Computing - Proceedings of AI*IA 2007 (10th Congress of Italian Association for Artificial Intelligence), Lecture Notes in Artificial Intelligence LNAI 4733, Springer, pp. 84 - 96, 2007.

## KLMLean 2.0: a Theorem Prover for KLM Logics of Default Reasoning

with Laura Giordano and Valentina Gliozzi

Kraus, Lehmann and Magidor (KLM) proposed a formalization of non-monotonic reasoning that was early recognized as a landmark. KLMLean 2.0 is a theorem prover implementing analytic tableaux calculi for all the logics of the KLM framework, namely (from the stringest to the weakest) rational logic R, preferential logic P, loop-cumulative logic CL, and cumulative logic C. It is written in SICStus Prolog and also comprises a GUI written in Java.

For more details, visit KLMLean web page

## Related publications:

Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, KLM Logics of Nonmonotonic Reasoning: Calculi and Implementations, In Giacomo Fiumara, Marco Marchi, Alessandro Provetti, Eds, Proceedings of the 22nd Italian Conference on Computational Logic (CILC 2007), 0, pp. 1 - 15, 2007.

Laura Giordano, Valentina Gliozzi, Gian Luca Pozzato, KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning, In Nicola Olivetti, Eds, Automated Reasoning with Analytic Tableaux and Related Methods - Proceedings of TABLEAUX 2007 (16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), Lecture Notes in Artificial Intelligence LNAI 4548, Springer, pp. 238 - 244, 2007.

Nicola Olivetti, Gian Luca Pozzato, KLMLean 1.0: a Theorem Prover for Logics of Default Reasoning, In Holger Schlingloff, Eds, Proceedings of the 4th International Workshop on Methods for Modalities (M4M-4), 0, pp. 235 - 245, 2005.

## CondLean 3.2: a Theorem Prover for Conditional Logics

with Nicola Olivetti

Conditional logics have a long history, and recently they have found several applications in artificial intelligence, such as deductive databases, nonmonotonic reasoning, belief revision. CondLean 3.2 is a theorem prover implementing some sequent calculi for these logics. It is written in SICStus Prolog and also comprises a GUI written in Java.

For more details, visit CondLean web page

## Related publications:

Nicola Olivetti, Gian Luca Pozzato, Automated Reasoning for Conditional Logics: the Theorem Prover CondLean 3.1, Perspectives on Universal Logic, , pp. 395 - 415, 2007.

Nicola Olivetti, Gian Luca Pozzato, CondLean: A Theorem Prover for Conditional Logics, In Marta Cialdea Mayer, Fiora Pirri, Eds, Automated Reasoning with Analytic Tableaux and Related Methods - Proceedings of TABLEAUX 2003 (12th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), Lecture Notes in Artificial Intelligence LNAI 2796, Springer, pp. 264 - 270, 2003.

Nicola Olivetti, Gian Luca Pozzato, CondLean 3.0: Improving Condlean for Stronger Conditional Logics, In Bernhard Beckert, Eds, Automated Reasoning with Analytic Tableaux and Related Methods - Proceedings of TABLEAUX 2005 (14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), Lecture Notes in Artificial Intelligence LNAI 3702, Springer, pp. 328 - 332, 2005.

Nicola Olivetti, Gian Luca Pozzato, Theorem Proving for Conditional Logics: CondLean and GoalDuck, Journal of Applied Non-Classical Logics 18(4), Taylor & Francis Online, pp. 427 - 473, 2008.

## DysToPic: a Distributed Theorem Prover for non–monotonic Description Logics

with Luca Violanti

Nonmonotonic extensions of Description Logics have been actively investigated since the early 90s. We have introduced a simple but powerful nonmonotonic extension of Description Logics in which typical properties can be directly specified by means of a typicality operator T enriching the underlying DL; the typicality operator T is essentially characterized by the core properties of nonmonotonic reasoning axiomatized by KLM preferential and rational logic. In these logics one can consistently express defeasible inclusions and exceptions such as: typical students do not pay taxes, but working students do typically pay taxes, but working students having children normally do not. DysToPic is distributed theorem prover for these logics. Expanding PreDeLo, the application is based on a SICStus Prolog implementation oftableaux calculi for ALC+T, wrapped by a Java interface which relies on the Java RMI APIs for the distribution. The system is designed for scalability and based on a "worker– employer" paradigm: the computational burden for the "employer" can be spread among an arbitrarily high number of "workers" which operate in complete autonomy, so that they can be either deployed on a single machine or on a computer grid.

DysToPic: application and source files