Formal Languages and Reasoning

From Wsmx-WIKI
Jump to: navigation, search
Navigation: Main Page | Members | Publications | References | Meetings

The Formal Languages and Reasoning group (FLaRe) consolidates and drives all research in the area of Knowledge Representation and Knowledge Processing at STI-Innsbruck. More specifically, Knowledge Representation on the Web and in Semantically-Enabled Service-Oriented Architectures (SESOA).


Descriptions in a Semantically-Enabled Service Oriented Architecture (SESOA) need different formal languages for the specification of different aspects of knowledge and services. The descriptions in a SESOA can be decomposed into four dimensions and it is our mission to develop and combine languages for these dimensions of description in a SESOA. In the process we will relate these languages to current and upcoming Semantic Web and Web Service languages.

  • Static knowledge (ontologies) are the core of the Semantic Web and of any Semantic Service Oriented Architecture. They can be used to formally describe any kind of knowledge on the Semantic Web and they form the vocabulary for the other dimensions fo description in a SESOA.
  • Functional description (capabilities) allow services to be viewed as functions which provide a certain output, given a particular input. This simplified view of services is useful for such tasks as discovery and composition.
  • Behavioural description (choreography/orchestration). Choreographies describe the interface of a service in terms of possible interactions with a service. Orchestrations describe compositions of services. Choreographies and Orchestrations can both be viewed as decompositions of capabilities.
  • Non-functional Properties* describe such things as author, natural language description, quality of service, pricing, service-level agreements, etc.

We will create an efficient and extensible software framework for reasoning with expressive rule-based languages (WSML-Core/Flight/Rule) as well as description logic based languages (WSML-DL). The reasoning framework will be based on state-of-the-art reasoning algorithms (for query answering, logical entailment, etc). The Semantic Execution Environment (SEE) needs the reasoning component for service discovery as well as both process and data mediation. Essential features of the reasoning framework are:

  • hybrid reasoning based on description logics and logic programming
  • reasoning with very large datasets
  • reasoning with heterogeneous and conflicting information
  • reasoning in distributed environments

Another major objective is the implementation of Rule Interchange Format (RIF). RIF aims to specify a common format for rules in order to allow rule interchange between diverse rule systems. This format (or language) will function as an interlingua into which rule languages can be mapped, allowing rules written in different languages to be executed in the same reasoner engine. The RIF layer of our reasoner engine will be capable of handling rules from diverse rule systems and will make WSML-Rule sets interchangeable with rule sets written in other languages that are also supported by RIF.


Current Status

The most important achievement so far is the specification of the Web Service Modeling Language v0.21, which is a language for the specification of different aspects of a SESOA. There are, however, some aspects lacking in the specification. The aspects which are lacking are mentioned in the following subsections.

Documents related to WSML can be found online at:

i. Static knowledge (ontologies)

The ontology component of WSML consists of five variants:

- WSML-Core - intersection of DL and LP

- WSML-Flight - based on the Datalog subset of F-Logic with negation under the perfect model semantics

- WSML-Rule - based on the Horn subset of F-Logic with negation under the well-founded semantics

- WSML-DL - based on the expressive Description Logic SHIQ

- WSML-Full - a full first-order language with nonmonotonic extensions, which is a superset of WSML-DL and WSML-Rule

Two main aspects are lacking in the ontology component of WSML:

- Semantics of WSML-Full. There is a preliminary proposal to use first-order autoepistemic logic as the language underlying WSML-Full, but this requires more investigation:

- Layering of WSML variants. A formal theorem stating the proper layering of WSML languages is lacking. Especially the layering between variants with ontology modeling based on predicates (WSML-Core, WSML-DL) and variants with ontology modeling based on frames (WSML-Flight, WSML-Rule, WSML-Full) has not been proven.

Other work which has been done by the participants of this research component:

- Development of a rule language for the semantic web: initial work has been done on scoped default negation, and members of this research component participate in the W3C RIF working group.

- Conceptual logic programs can be used to reason over expressive description logics, as well as certain combinations of description logic ontologies and rules

ii. Functional description (capabilities)

There is an initial proposal for functional description of services, based on abstract state spaces: This model can be used in combination with different logical languages.

Requirements are generally lacking.

iii. Behavioural description (choreography/orchestration)

The current language specification for choreography interfaces can be found at This specification is inspired from the ASM methodology and uses ontologies as the basic element for describing the states of interaction with the client. The language API has also been implemented as part of WSMO4J and is available from

iv. Non-functional Properties

There exists an initial discussion on the modeling and application of non-functional properties: within the WSML service description framework. This work is also highly related to external efforts around the modeling of context-aware services and their descriptions.

Future Steps

The following image depicts the relationship between the essentail description components of a SESOA and the relationship with current and future Semantic Web languages. Components with a black font are topics of active research within this research goal.


i. Static knowledge (ontologies)

Research on the representation of static knowledge will proceed along the following lines:

- Integrating knowledge based on classical first-order logic and nonmonotonic logic programming. Important issues are the representational adequacy of the integration, as well as decidable subsets and a proof theory, so that reasoning becomes possible.

- Decidable integration of Description Logics and Logic Programming from a Logic Programming perspective only (in constrast with WSML-Full), using open answer set programming with identification of algorithms. Investigation of non-standard reasoning such as finite satisfiability checking in the context of open answer set programming, with specifically in the languages component, the detection of fragments that are decidable for finite satisfiability checking.

- Definition of formalisms for distributed ontologies, specifically for logic programming based ontologies ( e.g., distributed open answer set programming). Application to discovery scenario with services in multiple distributed heterogenous repositories.

- Scoped default negation. When doing context-dependent reasoning, such as in nonmonotonic logic programming, the context is usually implicit. We aim to make to context explicit.

- Rules for the Semantic Web - participation in the RIF working group

- Connection between Semantic Web languages RDF, OWL

ii. Functional description (capabilities)

Requirements need to be gathered on the functional specification of services and a semantics needs to be devised which can be combined with the language for the description of ontologies, in order to enable the use of ontologies for the description of web service functionality. An important use case for the functional description of services is discovery. Therefore, it is expected that many requirements on the functional description of services will come from the discovery research goal.

iii. Behavioural description (choreography/orchestration)

There exist several formal languages which are suitable for describing the behavioral aspects of Semantic Web Services. Such languages include transaction logic, temporal logic and also action languages. We shall investigate the suitability of these languages with respect to the reasoning tasks defined for both choreography and orchestration. In particular for choreography interfaces, we shall focus on compatibility, that is, whether two (choreography) interfaces can communicate with each other successfully without any need of process mediation. We shall also give particular attention on the ease of use of the language such that it allows users to describe the interactions in the least modeling effort possible. A key challenge is also the combination of this language with ontology languages in order to enable the reuse of ontology vocabulary in the choreography and orchestration descriptions. Finally, this language will be connected to the language for capability descriptions in order to prove certain correspondences between the functional and behavioural description of services. We shall then ground this description to existing "syntactic" Web Service technologies such as WSDL.

iv. Non-functional Descriptions

Non-functional descriptions can at least be divided into two categories: (1) meta-data, e.g., author, description, etc., of the WSML statements in a description and (2) actual non-functional properties, i.e., actual properties of services (e.g. pricing, QoS, transactions). NFPs require a deeper investigation into their purpose and their usage. More precisely the following is needed: (1) requirements need to be gathered, (2) the language need to be defined by considering ontologies languages that allow nfps to be represented using ontologies, (3) integration with capability and bevaviour description languages


  • Explore the alternative approaches to applying well-founded semantics, particularly in combination with the magic sets transformation techniques.
  • Develop an algorithm for query containment with rule sets containing negation.
  • Reasoning with Rules for the Semantic Web - participation in the RIF working group
  • Reasoning with large and/or inconsistent data sets on a world scale.
  • New techniques for Description Logics reasoning.
  • Hybrid reasoning with DL/rules.

Software Implementations

The group actively develop several software components that are directly derived from the theoretical work conducted.

The software development guide describes the development process used within the group. This includes details of how each phase of a development life-cycle is conducted and what is output at each stage. Details of the peer-review (inspection) process, testing strategies and required documentation are also included.


  • IRIS (Integrated Rule Inference System) is a Datalog reasoner extended with locally stratified and well-founded negation, function symbols, unsafe-rules, built-in predicates and XML schema data types.
  • MINS (Mins is not Silri) is a Datalog reasoner extended with function symbols and well-founded negation. It is based on the SiLRI inference engine and is no longer supported.
  • RDFS Reasoner translates ontology descriptions in RDFS to predicates and rules. It is using IRIS as underlying reasoning engine and currently supports the RDF, RDFS and eRDFS entailment regimes.


  • WSMO4J Is an object model implementation of the WSML language and can be used to read, serialise and manipulate WSML documents.
  • WSML v0.21 validator - a syntactical validator for WSML v0.21, which validates a WSML specification against the WSML grammar and can validate and determine the WSML variant.


  • WSML2Reasoner is a highly modular framework that translates ontology descriptions in WSML to the appropriate syntax of several underlying reasoning engines.



Contributing Projects

Some of this work is funded by the European Commission and by the Austrian FIT-IT (Forschung, Innovation, Technologie - Informationstechnologie) under the following projects:

Deliverables Reminder

    • WP6
      • D6.9 Process Ontology and Query Reasoner – Final Implementation M30
      • D6.10 Integration of reasoning framework (WSML2Reasoner) M30
      • D6.13 Execution history M24
    • WP3
      • D3.2.1 Framework and APIs for integrated reasoning support (M6)
      • D3.2.2 First Prototype Repository reasoner for WSML-Core (M12)
      • D3.2.3 First Prototype Rule Reasoner for WSML-Rule (M18)
      • D3.2.4 First Prototype Description Logic Reasoner for WSML-DL (M18)
      • D3.2.5 Second Prototype Repository reasoner for WSML-Core (M24)
      • D3.2.6 Second Prototype Rule Reasoner for WSML-Rule (M30)
      • D3.2.7 Second Prototype Description Logic Reasoner for (M30)
  • LarKC
    • WP1
      • D1.1.2 Bridges to other areas (M12)
      • D1.1.3 Initial knowledge representation formalism (M6)
      • D1.3.1 Initial integration methodology (M18)
      • D1.3.2 Improved integration methodology (M33)
    • WP4
      • D4.4.1 Rule-based reasoning M24
      • D4.4.2 Implementation of above
    • WP5 (we are involved, but do not lead any of these)
      • D5.2.1 Rapid prototype M10 (M14) - CyC
      • D5.3.1 Requirements analysis and report on protoype M12 - HLRS
      • D5.3.2 Overall LarKC architecture and Design v1, M18 - HLRS
      • D5.3.3 Final LarKC architecture and Design v1, M36 - HLRS
      • D5.4.1 Initial release of LarKC platform M24 - HLRS
      • D5.4.2 Second release of LarKC platform M33 - HLRS
      • D5.4.3 Final release of LarKC platform M42 - HLRS


  • barry.bishop 'AT'
  • florian.fischer 'AT'

To post a message to all the list members, send email to: flare 'AT'