Unification in modal and description logics

被引:49
作者
Baader, Franz [1 ]
Ghilardi, Silvio [2 ]
机构
[1] Tech Univ Dresden, Dresden, Germany
[2] Univ Milan, I-20122 Milan, Italy
关键词
unification; description logics; modal logics; admissible rules; ADMISSIBLE RULES; COMBINATION; COMPLEXITY; VARIETIES; ALGORITHM; SYSTEM;
D O I
10.1093/jigpal/jzq008
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
Unification was originally introduced in automated deduction and term rewriting, but has recently also found applications in other fields. In this article, we give a survey of the results on unification obtained in two closely related, yet different, application areas of unification: description logics and modal logics.
引用
收藏
页码:705 / 730
页数:26
相关论文
共 75 条
[31]   Filtering unification and most general unifiers in modal logic [J].
Ghilardi, S ;
Sacchetti, L .
JOURNAL OF SYMBOLIC LOGIC, 2004, 69 (03) :879-906
[33]   A resolution/tableaux algorithm for projective approximations in IPC [J].
Ghilardi, S .
LOGIC JOURNAL OF THE IGPL, 2002, 10 (03) :229-243
[34]   Unification through projectivity [J].
Ghilardi, S .
JOURNAL OF LOGIC AND COMPUTATION, 1997, 7 (06) :733-752
[35]  
Goranko V., 1992, Journal of Logic and Computation, V2, P5, DOI 10.1093/logcom/2.1.5
[36]  
HERZIG A, 1989, THESIS U P SABATIER
[37]  
Horrocks Ian., 2000, LOG J IGPL, V8, P239, DOI DOI 10.1093/JIGPAL/8.3.239
[38]  
Iemhoff R, 2003, LECT NOTES COMPUT SC, V2803, P255
[39]   On the admissible rules of intuitionistic propositional logic [J].
Iemhoff, R .
JOURNAL OF SYMBOLIC LOGIC, 2001, 66 (01) :281-294
[40]   Proof theory for admissible rules [J].
Iemhoff, Rosalie ;
Metcalfe, George .
ANNALS OF PURE AND APPLIED LOGIC, 2009, 159 (1-2) :171-186