icona theorem proversTheorem Provers

Implemented Theorem Provers:

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 icona link esterno

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. icona file pdf

  • 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 icona link esterno

    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. icona file pdf

  • 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. icona file pdf

  • 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 icona link esterno

    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. icona file pdf

  • 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 icona link esterno

    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. icona file pdf

  • 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. icona file pdf

  • 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 icona link esterno

    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 icona link esterno

    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. icona file pdf

  • 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 icona link esterno

    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. icona file pdf

  • 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 icona link esterno

    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. icona file pdf

  • 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. icona file pdf

  • 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. icona file pdf

  • 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 icona link esterno

    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. icona file pdf

  • 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. icona file pdf

  • 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 icona file compresso 7z