Algebraic semantics for logic programs with negation
| Project/Area Number |
15500016
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Tokyo Denki University |
|---|
Principal Investigator |
KONDO Michiro Tokyo Denki University, information Environment, Professor, 情報環境学部, 教授 (40211916)
|
|---|
| Project Period (FY) |
2003 – 2005
|
| Project Status |
Completed (Fiscal Year 2005)
|
| Budget Amount *help |
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 2005: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2004: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2003: ¥1,000,000 (Direct Cost: ¥1,000,000)
|
|---|
| Keywords | bilattice / residuated t-norm / categorically equivalent / BCK-algebra / fuzzy logic / congruence / fixed point theorem / 不動点意味論 / 様相演算子 / t-norm / prime bifilter / quotient algebra / BCK / BCI-algebra / transfer principle / ideal |
|---|
| Research Abstract |
In the theory of logic programs with negation, the Knaster-Tarski's fixed point theorem does not hold in general because of adding a new operation "negation" to programs. To overcome the difficulty, it is added a new order to the original algebraic system such that the negation operator is monotone with respect to the new order. As a result, the algebraic systems have two kinds of orders and hence it is called "bilattices". Typical bilattices called "interlaced bilattices" play an important role to develop the theory of algebraic semantics of logic programs. Recently, it has proved that those are isomorphic to the Ginsberg product of bounded lattices. The aim of my research is to generalize the theory of bilattices to apply it to more general programs such as ones with negation and more operators. Since the negation is presented by an implication symbol, I introduced the implication operator in partially ordered sets as a right adjoint operator of a new product ^*. Partially ordered sets are more general algebraic systems than lattices. The product operator is called a residuated t-norm in the theory of fuzzy logics. If some extra axioms are added to the partially ordered set with residuated t-norm, then the algebraic system is called a lattice implication algebra. I could prove that the class of lattice implication algebras coincided with the one of commutative bounded BCK-algebras. Moreover I could prove that the class of bounded partially ordered sets with residuated t-norm was categorically equivalent to the one of bounded BCK-algebras with condition (S). The result means that we can use the Ginsberg product of bounded BCK-algebras with condition (S) as an algebraic semantics of logic programs with negation and more operators.
|
Report
(4 results)
Research Products
(22 results)
