turkmath.org

Both from the theoretical viewpoint and the viewpoint of applications, inference rules in nonstandard logics give rise to many interesting problems. One of them is the determination of their admissibility. Admissible inference rules do not depend on the choice of an axiomatic systems for a given logic and constitute the greatest set of rules compatible with its derivability relation. Logic being the science of reasoning, deciding the admissibility property in such or such logic is a research topic of the utmost interest for those who want to improve the efficiency of automated deduction. The admissibility problem in modal logics is strongly related to another problem of interest, the unification problem. As the admissibility problem, the unification problem in modal logics has been motivated by automated deduction tools. Its starting point was the existence of a most general unifier for any unifiable formula in Boolean Logic. Later it was proved that in general, there are no most general unifiers for unifiable formulas in various modal logics but a finite set of maximal unifiers. These results provide a connection between unification of formulas and admissibility of inference rules. I will talk on this relationship between admissibility and unifiability.