Algebraic semantics for logic programs with negation

在带否定的逻辑程序理论中，由于在程序中增加了一个新的运算“否定”，Knaster-Tarski不动点定理一般不成立。为了克服这一困难，在原代数系统中增加了一个新的阶，使得否定算子关于新的阶是单调的。结果，代数系统有两种阶，因此它被称为“双格”。典型的双格称为“交错双格”，它对逻辑程序代数语义理论的发展起着重要的作用。最近，证明了它们同构于有界格的Ginsberg积。我的研究目的是推广双格理论，将其应用于更一般的程序，如具有否定和更多操作符的程序。由于否定是由蕴涵符号表示的，我引入了偏序集上的蕴涵算子作为新积^* 的右伴随算子。偏序集是比格更一般的代数系统。乘积算子在模糊逻辑理论中被称为剩余t-范数。如果在具有剩余t-范数的偏序集上增加一些额外的公理，则该代数系统称为格蕴涵代数。证明了格蕴涵代数类与交换有界BCK-代数类是一致的。证明了具有剩余t-范数的有界偏序集类与具有条件（S）的有界BCK-代数类是范畴等价的。这个结果意味着我们可以把有界BCK-代数的条件（S）的Ginsberg积作为具有否定和多算子逻辑程序的代数语义。

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.