OntologyUtils: ontology engineeringSee project here. It contains a suite of utility functions and applications for engineering OWL ontologies.
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.
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.
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).
Some NuSMV code here. It shows a mistake in (Balbiani, Herzig, Troquard 2013).
Miscellaneous public projects on bitbucket.