MALFO serialization

This repo contains various serializations of the ontology MALFO (MALFunction Ontology):

• first-order logic: MALFO is serialized in the languages clif (Common Logic Interchange Format), tptp (Thousands of Problems for Theorem Provers format), and p9 (Prover9). The clif version was parsed with The .clif axioms were parsed with macleod: https://github.com/thahmann/macleod. With the same tool the tptp and p9 version were generated automatically.
• disjunctive datalog: MALFO is serialized in a disjunctive datalog language (MALFO.pl has been parsed with DLV). Note that MALFO.pl contains a program roughly equivalent to first-order MALFO (the signature of DLV MALFO has been expanded with auxiliary predicates to realize the equivalence: these should be removed if used in applications, especially those participating in existential rules, otherwise there is the risk of slow or non-terminating program executions).
• OWL: a manually-curated reduction of first-order MALFO to OWL is present in MALFO.owl. Testing of reasoning happened on Protegé 5.5.0, with Hermit 1.4.3.456: note that bugs with reasoning tasks were found using more recent version of Protegé. Moreover, note that an ad-hoc reasoning system has been implemented, bypassing the need for (complete but cumbersome) OWL reasoning. The ad-hoc reasoning is implemented through queries, so that its application to, say, a graph on a triplestore would be convenient. To execute such reasoning, run `infer.py' and input the name of any file containing an instantiation of MALFO OWL ontology. A corresponding output file with the inferences materialized will be created. Domain and range axioms will also be checked.

Consistency and satisfiability of classes of the first-order theory has been confirmed using Vampire through the "Systems on TpTp" tool available at: https://www.tptp.org/cgi-bin/SystemOnTPTP, while the OWL theory has been applied to some models.

MALFO Taxonomy

The taxonomy of MALFO, obtained with Plant UML:

MALFO taxonomy, vertical orientation

MALFO taxonomy, horizontal orientation

MALFO mappings

Note that take has been taken that MALFO is an ontological module that can be aligned with ease with other ontologies, in the sense that the eventual mappings between MALFO and the other ontologies should be small. There is also an exemplificative alignment with the DOLCE-based theory of functions from https://github.com/kataph/function-method-ontology. The alignment is contained in the file "MALFO-plus-DOLCE-functions.owl", which imports MALFO, an OWL version of DOLCE, and the OWL version of the DOLCE-based theory of functions. The latter two files are from the function-method-ontology repository and have been duplicated here for sake of simplicity.

MALFO models

The models have been encoded in graphml files for the sake of visual presentation. A script, `read_graphml.py' is supplied that converts these into knowledge graphs. The script assumes that the input files have the xml structure of documents generated by the (3.23.2) yEd desktop app and follow the same convention in terms of mapping shapes, colors, and edge labels to MALFO OWL terms. In particular, the script is not intended to replace an ontology editor. To convert a graphml file, simply run the script and input the name or path of the graphml file. A corresponding output file will be created.

Some visualizations of some examples:

Visualization of the 'Matthews-1.graphml diagram'. Schematization of the fracture of an industrial fan main shaft considered from "A Practical Guide to Engineering Failure Investigation", Clifford M., 1998. Red nodes are function-incompatible occurrences. The MALFO’s class of an occurrence is put between double angle quotation marks (“«” and “»”)

Visualization of the 'Matthews-2.graphml diagram'. Another conceptualization of the same failure event. The arrows in red denote corrections facilitated by the reasoning process, see next section. The numbers in the small dia

Visualization of the 'Avizienis.graphml diagram'. Schematization of a failure in an integrated circuit due to a short circuit, as considered in "Basic Concepts and Taxonomy of Dependable and Secure Computing", Avizienis A. et al., 2004. The top row is Avizienis’ original conceptualization, the bottom row is a revised conceptualization using Toyoshima’s causation ontology (used by MALFO). Dashed lines between the two conceptualizations link corresponding occurrences. Red nodes are function-incompatible occurrences. The MALFO’s class of an occurrence is put between double angle quotation marks (“«” and “»”)

MALFO Reasoning

Using MALFO to represent failure cases enables the use reasoning. For instance, one can carry out classification of occurrences into the classes of MALFO taxonomy in an explainable way, starting from information about functions, ontological categories, and causal relations; and check the consistency of the model w.r.to MALFO's axioms. For instance, in the visualization of matthews-2.graphml above, some arrows are red. This indicates that those arrows are corrections of errors individuated by explanations of inconsistency generated by a reasoner.

One such explanation of inconsistency: the arrow "achieves" was wrong due to the violation of domain/range constraints. Therefore it was corrected in the diagram

Biblio

For more info see Ontological Analysis of Malfunctions: Some Formal Considerations, Compagno Francesco, Stefano Borgo. In the proceedings of Formal Ontology in Information Systems 2024.