# Software

## 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.

## 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.