Unification in modal and description logics

被引:48
作者
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 条
[21]   UNIFICATION IN BOOLEAN RINGS AND ABELIAN-GROUPS [J].
BOUDET, A ;
JOUANNAUD, JP ;
SCHMIDTSCHAUSS, M .
JOURNAL OF SYMBOLIC COMPUTATION, 1989, 8 (05) :449-477
[22]   DISCRIMINATOR VARIETIES AND SYMBOLIC COMPUTATION [J].
BURRIS, S .
JOURNAL OF SYMBOLIC COMPUTATION, 1992, 13 (02) :175-207
[23]  
CAMPBELL JR, 2007, P 12 WORLD C HLTH ME, P2401
[24]   An NP decision procedure for protocol insecurity with XOR [J].
Chevalier, Y ;
Küsters, R ;
Rusinowitch, M ;
Turuani, M .
18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, :261-270
[25]   Intruder deductions, constraint solving and insecurity decision in presence of exclusive or [J].
Comon-Lundh, H ;
Shmatikov, V .
18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, :271-280
[26]   A survey of algebraic properties used in cryptographic protocols [J].
Cortier, Veronique ;
Delaune, Stephanie ;
Lafourcade, Pascal .
JOURNAL OF COMPUTER SECURITY, 2006, 14 (01) :1-43
[27]  
del Cerro L. F., 1989, MACHINE LEARNING MET, P301
[28]   Easy intruder deduction problems with homomorphisms [J].
Delaune, S .
INFORMATION PROCESSING LETTERS, 2006, 97 (06) :213-218
[29]  
Dzik W, 2006, CONTRIB GEN ALGEBRA, V17, P73
[30]  
FRIEDMAN H, 1975, J SYMBOLIC LOGIC, V40, P113, DOI 10.2307/2271891