Unification in intuitionistic logic

被引：121

作者：

Ghilardi, S ^{[1
]}

机构：

[1] Univ Milan, Dipartimento Sci Informaz, I-20135 Milan, Italy

来源：

JOURNAL OF SYMBOLIC LOGIC | 1999年 / 64卷 / 02期

关键词：

E-unification; projective Heyting algebras; exact formulas; admisssible inference rules;

D O I：

10.2307/2586506

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

引用

页码：859 / 880

页数：22

共 23 条

[1] BAADER F, 1993, HDB LOGIC ARTIFICIAL, P41
[2] INJECTIVE AND PROJECTIVE HEYTING ALGEBRAS
BALBES, R
HORN, A
[J]. TRANSACTIONS OF THE AMERICAN MATHEMATICAL SOCIETY, 1970, 148 (02) : 549 - &
[3] THE DECIDABILITY OF DEPENDENCY IN INTUITIONISTIC PROPOSITIONAL LOGIC
DEJONGH, D
CHAGROVA, LA
[J]. JOURNAL OF SYMBOLIC LOGIC, 1995, 60 (02) : 498 - 504
[4] DEJONGH D, 1982, LEJ BROUWER CENTENAR, P51
[5] DEJONGH DHJ, 1996, LOGIC FDN APPL, P187
[6] LOGICS CONTAINING K4 .2.
FINE, K
[J]. JOURNAL OF SYMBOLIC LOGIC, 1985, 50 (03) : 619 - 651
[7] FINE K, 1974, J SYMBOLIC LOGIC, V34, P31
[8] GABBAY DM, 1981, SINTHESE LIB, V148
[9] A SHEAF REPRESENTATION AND DUALITY FOR FINITELY PRESENTED HEYTING ALGEBRAS
GHILARDI, S
ZAWADOWSKI, M
[J]. JOURNAL OF SYMBOLIC LOGIC, 1995, 60 (03) : 911 - 939
[10] Unification through projectivity
Ghilardi, S
[J]. JOURNAL OF LOGIC AND COMPUTATION, 1997, 7 (06) : 733 - 752

← 1 2 3 →