Non-Canonical Automated Deduction

The project presented here belongs to the Automated Deduction field. This deals with the problem of, having a particular explicit knowledge specified in a certain formal language and a set of inference rules, deducing new knowledge implicit in the Knowledge Base that follows logically from this one and which is relevant for the application at hand.

Currently, there is a increasing demand of a \emph{Deductive Software} in many applications such as Deductive Data Bases, Logic Programing, Expert Systems, Safety Critical Systems, Real Time Systems, Robotics, Multi-agents Systems, Processes Control, etc.

Given the large variety of types of knowledge required in the diverse cognitive areas, different representation formalisms are being considered by the research community. Thus, in this project we shall explore several representation formalisms including classical languages and languages recently emerged. We will analyse also the way in which these formalisms characterise the inference rules and the way of chaining them efficiently in a deductive process.

The languages that will be studied are inside the non-canonical logic and more specifically, we will deepen in the deductive systems based on

• Non-clausal forms
• Theories with special binary connectives
• Unification in non-canonical contexts
• Diagrammatic syntax

A la página de GIMAC