Fuzzy Reasoning Engine FiRE

Table of Contents

1. Description
2. Installation Instructions
3. User Manual
3.1 DL Operators
3.2 Fuzzy DL SHIN Syntax
3.2.1 TBox Declaration
3.2.2 Axioms Declaration
3.2.3 ABox Declaration
3.3 An Example
3.4 Run Menu
3.4.1 Complile
3.4.2 ABox Consistency
3.4.3 Classification
3.4.4 Global glb
3.4.4 Global glb path
3.4.6 Options
3.5 Query Panes
3.5.1 Entailment Check
3.5.2 Subsumption Check
3.5.3 Greatest lower bound
3.6 Information Panes
3.6.1 Tableaux Expansion Pane
3.6.2 Output Pane
3.6.3 Tableaux Pane
3.6.4 Model Pane
3.6.5 Classification Pane
4. Future Extensions
5. Contact Details
 

1. Description

This is a research software implemented by Nikolaos Simou based on the research of G.Stoilos, G.Stamou et all publised in the paper The Fuzzy Description Logic f-SHIN.

Description Logics formalism is a modern knowledge representation language that has gained considerable attention the last decade. Today many applications use Description Logics (DLs) to represent knowledge and to perform reasoning tasks in order to deduce new knowledge out of the explicitly stated one. Some examples are , the Semantic Web, multimedia and image processing, medical informatics, databases and many more. A problem that occurs in many of these domains is a huge amount of imprecise and vague knowledge and information. The current implementation is an extension of DL SHIN with fuzzy set theory that allows the management of such information.

2. Installation Instructions

The software was implemented using Java2 and it is a JAR executable. In order to execute a jar file you first have to install Java (http://java.sun.com/j2se/1.4.2/download.html), then you execute the jar file by the command "java –jar FiRE.jar". For optimum performance it is recommended 512M to be allocated to the application, this can be done by the command "java –jar –Xms512M –Xmx512M FiRE.jar"

Download FiRE

3. User Manual

The following table presents the operators currently used by FiRE. The FiRE syntax requires all the statements to be enclosed by brackets, and in detail the syntax of the operators is shown on the left column with the keywords denoted in red colour. Note that the result of any DL operator is a concept and this makes possible the use of many DL operators for the creation of a concept. (See Axioms Declaration)

3.1 DL Operators

Syntax Description
*top* Top concept
*bottom* Bottom concept
(not concept) General negation
(and concept1... conceptN) Conjuction
(or concept1... conceptN) Disjunction
(some role concept) Exist restriction
(all role concept) Value restriction
(at most n role) At most restriction
(at least n role) At least restriction

3.2 Fuzzy DL SHIN Syntax

A DL knowledge consists of the Terminological Formalism (TBox) and the Assertional Formalism (ABox). TBox includes the concepts, the individuals to which concepts participate, and the roles that connect the individuals. On the other hand ABox includes the assertions. The following tables illustrate the syntax of the DL SHIΝ with fuzzy extensions.

3.2.1 TBox Declaration

Terminology box is required for a knowledge and defines the concepts the roles and the individuals. TBox declaration is made using the keyword signature and it is divided into three smaller declarations the concepts declaration using keyword atomic-concepts, the roles declaration using keyword roles and the individuals declaration using keyword individuals. The following table shows a TBox declaration on the left column with explanatory comments on the description column.

Syntax Description
(signature :atomic-concepts (human person female male woman man mother father grandmother aunt uncle sister brother only-child cry) TBox declaration starts with keyword signature. Concepts are declared using keyword atomic-concepts followed by the concept names separated by space within brackets .
:roles ((has-gender :transitive t)

(has-descendant :transitive t)

(has-child :inverse has-descendant

:domain parent

:range person)

(has-sibling :domain (or sister brother)

:range (or sister brother))

(has-sister :inverse has-sibling

:range (some has-gender female))

(has-brother :inverse has-sibling

:range (some has-gender male))

)

Roles are declared using keyword roles. Each role is defined within brackets and it may have one or more of the following parameters

 

Keyword Description Syntax
parent States the parent role :parent parentRole
transitive States whether the role is transitive or not. (A role is not transitive by default) :transitive t

:transitive f

inverse States the inverse role of a role.( All roles have an inverse role and if it is not stated directly then it is Inv-roleName e.g for role has-child inverse role by default is Inv-has-child) :inverse invRole
domain States the concept type that is the role domain. :domain concept
range States the concept type that is the role range. :range concept

Note that domain and range are not fully supported

:individuals (alice betty charles doris eve)) Individuals are declared using keyword individuals followed by the individual names separated by space within brackets.

3.2.2 Axioms Declaration

There are two kinds of axioms implicitly and equivalence. The following table shows the way that these axioms can be defined. Note that equivalence axioms do not require concept1 to de defined in atomic concepts.

Syntax (implies/equivalent concept1 concept2) Description
(implies person (and human (some has-gender (or female male))))

(implies man (and person (some has-gender male)))

(equivalent father-having-only-sons (and man (all has-child man)))

(equivalent parent-having-many-children (and parent (at-least 3 has-child)))

Person

Man

father-having-only-sons

parent-having-many-children

3.2.3 ABox Declaration

Syntax (instance individual concept ⋈ degree) Description
(instance charles brother)

(instance charles brother >= 0.7 )

brother(charles) >= 1.0 (Crisp)

brother(charles) >= 0.7

Syntax (related individual1 individual2 role ⋈degree ) Description
(related alice betty has-child )

(related alice betty has-child >= 0.8 )

has-child(alice,betty) >= 1.0 (Crisp)

has-child(alice,betty) >= 0.8

3.3 An Example

Medical image processing and analysis is a highly emerging research area in bio-informatics technology. Let us here consider the applications of decision support in neurology and neurosurgery by processing of MRI (Magnetic Resonance Imaging) images, which has gained considerable attention. The process usually involves two steps. In the first step the MRI image is automatically segmented into areas, each one associated with a set of features like the length and depth of a sulcus segment in a brain cortex, the connection of two sulcus segments etc. The second step involves the identification and labelling of the different parts of the brain cortex, based on the segmented parts. Between these two faces, the identification step is the most difficult one.

Download MRI.fire

(More examples can be found here)

Open the file by selecting Open from the File menu and then select ABox Consistency from the Run Menu in order to check whether the knowledge is satisfiable. The output of the system can be shown in the figure below.

PrinScreen1

The GUI of the application is divided into three smaller regions. On the top left corner is the editor window, on the bottom the information panes and on the right the query panes.

3.4 Run Menu

3.4.1 Complile

Checks the knowledge for syntax errors that will be displayed in the Output pane. In case of no errors the statements declared are shown in the Output pane.

3.4.2 ABox Consistency

Checks the knowledge for consistency. In case of consistent knowledge the tableaux expansion pane presents the tableaux expansion in detail showing all the operators applied, the output pane shows the statements declared, tableaux pane shows the results of tableaux expansion and model pane the resulting model. In case of not consistent knowledge, tableaux expansion until the occurrence of clash is shown in tableaux expansion pane.

3.4.3 Classifiaction

This action performes subsumption check of all the posible combinations of concepts and it creates the taxonomy tree shown in Classification Pane.

3.4.4 Global glb

This action creates a file (filename.glb) with the the greatest lower bound of all concepts participating in all individuals. The format of the file is "individual;concept;gld;\n" for all the combinations of concepts with individuals.

3.4.5 Global glb path

Sets the path of the global glb file. If global gld path has not been set then glb file is saved as "globalGlb.glb" in the home directory.

3.4.6 Options

The user can change the priority number of the rules applied by selecting Options from the Run menu. A rule with higher priority number will execute before a rule with a lower priority number. To set the number double click to the relative cell from the priority column. (The priority number for each triple can be shown at Tableaux Pane and Tableaux Expansion Pane with symbol pN)

3.5 Query Panes

3.5.1 Entailment Check

The user can check whether a concept participates in an individual e.g.  whether o2 participates to IFGyrus by a degree greater or equal to 0.85 by entering ( instance o2 IFGyrus >= 0.85) to entailment input textfield. The syntax of entailment checks is flexible and can be of the form (instance individual concept ⋈ degree) or of the form individual concept ⋈ degree (i.e o2 IFGyrus >= 0.85 ).

3.5.2 Subsumption Check

A user can check whether a concept implies another concept by subsumption check. In our example user can check whether OPIFGyrus is subconcept of ( some isDAPartOf IFGyrus) by entering ( implies OPIFGyrus ( some isDAPartOf IFGyrus)) to subsumption input textfield. The syntax of subsumption checks is flexible and can be of the form (implies concept1 concept2) or of the form (concept1) (concept2) (i.e (OPIFGyrus) ( some isDAPartOf IFGyrus)).

3.5.3 Greatest lower bound

A user can evaluate using this function the greatest lower bound of a concept participating in an individual. The glb of IFGyrus in individual o2 can be evaluated by entering ( instance o2 IFGyrus ) to glb input textfield. The syntax of entailment checks is flexible and can be of the form (instance individual concept) or of the form individual concept (i.e o2 IFGyrus).

3.6 Information Panes

3.6.1 Tableaux Expansion Pane

Shows the tableaux expansion presenting all the details concerning the rules that were applied.

3.6.2 Output Pane

Presents compilation errors and in the case that there are not any it shows the concepts and the roles declared together with their attributes.

3.6.3 Tableaux Pane

Presents the satisfiable tableaux.

3.6.4 Model Pane

Presents a model of the satisfiable tableaux.

3.6.5 Classification Pane

Presents the tree of the concepts taxonomy.

4. Future Extensions

  • Extend to other uncertainty formalisms. Studying and integrating other types of uncertainties is one of our future goals.
  • Extend the DL component’s expressiveness. FiRE supports a fuzzy version of the DL language SHIN. SHIN is expressive, but algorithms for even more expressive DL languages, such as SHOIQ, exist.
  • Extend the fuzzy component’s expressiveness. FiRE supports the Zadeh fuzzy version of SHIN, fKD-SHIN. Apart from the Zadeh fuzzy operators, several others result in different logical properties.
  • Support data types. FiRE doesn’t yet support data types. Proposals exist for fuzzy data type expressions, such as “about 15,” a data type defined as a fuzzy set around the value 15.
  • Support rules. Previous efforts have mainly focused on providing a rule interchange format rather than a single rule language, but several proposals for a Semantic Web rule language exist. Integrating fuzzy rules with fuzzy DLs is another interesting extension.

5. Contact Details

For any problems or suggestions please contact Nick Simou.

Copyright Image Video and Multimedia Systems Lab (IVML)