Theorem Provers

VINTE

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, pages 149-159, Springer, 2017.

NESCOND: an implementation of nested sequent calculi for Conditional Logics

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

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

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

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

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

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

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

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, 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

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.

Related publications:

Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, Luca Violanti, DysToPic: a Multi-Engine Theorem Prover for Preferential Description Logics, In Diego Calvanese and Boris Konev, Eds, Proceedings of the 28th International Workshop on Description Logics, Athens,Greece, June 7-10, 2015. CEUR Workshop Proceedings 1350, CEUR-WS.org 2015.

COCOS

COCOS (a typicality based COncept COmbination System) is a tool developed in order to account for the phenomenon of combining prototypical concepts, an open problem in the fields of AI and cognitive modelling. COCOS is based on a probabilistic extension of a Description logic of typicality, allowing to express inclusions of the form p :: T(C) ⊑ D ("we have probability p that typical Cs are Ds") and it embeds a set of cognitive heuristics for concept combination. COCOS is written in Pyhton and exploits HermiT for reasoning in the underlying standard Description Logic ALC.

For more details, visit COCOS web page

Related publications:

Antonio Lieto, Gian Luca Pozzato, Alberto Valese, COCOS: a typicality based COncept COmbination System, In Paolo Felli and Marco Montali, Eds, Proceedings of CILC 2018 - 33rd Italian Conference on Computational Logic, CEUR Workshop Proceedings 2214, CEUR-WS.org 2018, Bolzano, Italy, September 20-22, 2019.

GOCCIOLA

GOCCIOLA (Generating knOwledge by Concept Combination In descriptiOn Logics of typicAlity) is a tool for the dynamic generation of novel knowledge by exploiting an extension of a Description Logic of typicality able to combine prototypical descriptions of concepts. Given a goal expressed as a set of properties, in case an intelligent agent cannot find a concept in its initial knowledge base able to fulfill all these properties, GOCCIOLA exploits a Description Logic with typicality and probabilities in order to find two concepts whose creative combination satisfies the goal. The knowledge base of the agent is then extended by the prototype resulting from the concept combination, and the combined concept represents the solution for the initial goal.

For more details, visit GOCCIOLA web page

Related publications:

Antonio Lieto, Federico Perrone, Gian Luca Pozzato, GOCCIOLA: Generating New Knowledge by Combining Concepts in Description Logics of Typicality, In Alberto Casagrande and Eugenio G. Omodeo, Eds, Proceedings of CILC 2019, the 34th Italian Conference on Computational Logic, Trieste, Italy, June 19-21, 2019. CEUR Workshop Proceedings 2396, CEUR-WS.org 2019.

PEAR

PEAR (Probability of Exceptions and typicAlity Reasoner) is a tool for reasoning about prototypical properties in an extension of Description Logics of typicality with probabilities and scenarios. In this logic, different scenarios are considered by taking into account several extensions of the ABox, containing only some typicality assumptions about individuals. Each scenario has a probability depending on those equipping typicality inclusions, then entailment can be restricted to scenarios whose probabilities belong to a given and fixed range. PEAR is implemented in Python, it computes all scenarios of a knowledge base and it allows the user to check the probability of a query by exploiting a translation into standard ALC.

For more details, visit PEAR web page

Related publications:

Gian Luca Pozzato, Gabriele Soriano, PEAR: a Tool for Reasoning About Scenarios and Probabilities in Description Logics of Typicality, In Alberto Casagrande and Eugenio G. Omodeo, Eds, Proceedings of CILC 2019, the 34th Italian Conference on Computational Logic, Trieste, Italy, June 19-21, 2019. CEUR Workshop Proceedings 2396, CEUR-WS.org 2019.

PRONOM

Non-Normal Modal Logics have been studied since the seminal works by Lewis, Scott, Lemmon, and Chellas in the 1960s. They are a generalization of ordinary modal logics that do not satisfy some axioms or rules of minimal normal modal logic K. They have gained interest in several areas such as epistemic and deontic reasoning, reasoning about games, and reasoning about "truth in most of the cases". PRONOM (theorem PROver for NOnnormal Modal logics) is a theorem prover for the classical cube of non-normal modal logic. It is written in SWI Prolog and can be used by means of a web interface.

For more details, visit PRONOM web page