IRGPY: Resource Contribution Games

Tools for finding Nash equilibria solutions in some classes of the resource contention games.

References:

  • Nicolas Troquard. Existence and verification of Nash equilibria in non-cooperative contribution games with resource contention. In Annals of Mathematics and Artificial Intelligence , 92, pages 317–353. Springer, 2024. [ springer open access ]
  • Nicolas Troquard. Nash equilibria and their elimination in resource games. In 25th International Joint Conference on Artificial Intelligence (IJCAI 2016). AAAI Press, 2016, pages 503-509. [ .pdf | ijcai ]

See project here.

randonto

Randomly generate parameterized basic OWL ontologies.

See project here. It can work hand-in-hand with the app AppCheckConsistencyBasic from the OntologyUtils project.

OntologyUtils: ontology engineering

See project here. It contains a suite of utility functions and applications for engineering OWL ontologies.

The function MaximalConsistentSets#maximalConsistentSubsets takes a set of axioms in parameter and returns the set of maximally consistent subsets. It is an implementation of the algorithm presented in the paper Robert Malouf: Maximal Consistent Subsets, Computational Linguistics, vol 33(2), p.153-160, 2007.

The app AppNormalization takes as input any OWL ontology whose TBox can be transformed into subclass axioms (subclass, equivclass, disjointunion, disjointclass, property domain, property range). It produces an "equivalent" version of the ontology in the form of normalized rules. There's a naive method for the normalization, and the normalization method presented in the paper Frantisek Simancik, Yevgeny Kazakov, Ian Horrocks: Consequence-Based Reasoning beyond Horn Ontologies. IJCAI 2011: 1093-1098 as well.

The class RefinementOperator contains an implementation of the refinement operators presented in Nicolas Troquard, Roberto Confalonieri, Pietro Galliani, Rafael Peñaloza, Daniele Porello, Oliver Kutz: Repairing Ontologies via Axiom Weakening. AAAI 2018. The class AxiomWeakener implements the axiom weakening operations: AxiomWeakener:getWeakerSubClassAxiom is used for subclass axioms, and AxiomWeakner:getWeakerClassAssertionAxioms is used for assertion axioms. A few apps showcase the axiom weakening method for ontology repair: see, AppAutomatedRepairRandomMCS, AppAutomatedRepairWeakening, AppAutomatedRepairWeakening, AppInteractiveRepair, and AppInteractiveReferenceOntologyAndRepair.

The class TurnBasedMechanism contain an implementation of the multiagent turn-based approach for ontology aggregation presented in Daniele Porello, Nicolas Troquard, Rafael Peñaloza, Roberto Confalonieri, Pietro Galliani, and Oliver Kutz. Two Approaches to Ontology Aggregation Based on Axiom Weakening. IJCAI-ECAI 2018. The app AppTurnBasedMechanism showcases it.

The class BlendingDialogue contain an implementation of the algorithm for creating asymmetric hybrid concepts in Guendalina Righetti, Daniele Porello, Nicolas Troquard, Oliver Kutz, Maria M. Hedblom, and Pietro Galliani. Asymmetric Hybrids: Dialogues for Computational Concept Combination. FOIS 2021. The app AppBlendingDialogue showcases it.

Reasoning about social choice functions

This is a LISP implementation of the logic from the research paper Nicolas Troquard, Wiebe van der Hoek, Michael Wooldridge: Reasoning About Social Choice Functions, J. Philosophical Logic 40(4): 473-498 (2011). The logic allows one to talk about social choice functions, preferences of agents and their choices in a rigorous way. The software assists the user in defining social choice functions, agent profiles, and the characterization of strategic equilibria such as the Nash equilibrium or dominance equilibrium. It permits the verification of game properties and the search of strategic equilibria. It also permits to verify whether a social choice function is strategy-proof.

A succinct description of the theoretical background of the software is presented here. See the code here.

Provers for modal Linear Logic

This is a proof of concept written in PROLOG for the logical frameworks presented in the research papers Daniele Porello, Nicolas Troquard: Non-normal modalities in variants of Linear Logic, Journal of Applied Non-Classical Logics 25(3): 229-255 (2015) and Daniele Porello, Nicolas Troquard: A resource-sensitive logic of agency, ECAI 2014: 723-728. mllprover is a simple extension of Naoyuki Tamura's Linear Logic Prover with a non-normal modality. individual biat prover is another extension with a set of modalities of bringing-it-about. It allows one to prove formal statements about resource-sensitive socio-technical systems.

See details and code here.

ProSaBa: PROlog SAt-BAsed

ProSaBa is a PROLOG implementation of the SAT-based algorithm to determine the satisfiability of multi-modal (multi-K) propositional formulas.

See details here. The code is presented in this document (in French).

MISC

Some NuSMV code here. It shows a mistake in (Balbiani, Herzig, Troquard 2013).

Miscellaneous public projects on bitbucket.