Algebraic semantics for logic programs with negation

在具有否定的逻辑程序理论中，由于在程序中增加了一个新的运算“否定”，使得Knaster-Tarski不动点定理不再普遍成立。为了克服这个困难，在原代数系统中增加了一个新阶，使得负算子相对于新阶是单调的。因此，代数系统具有两种阶数，因此称为“双格”。被称为“交错双格”的典型双格在逻辑程序代数语义理论的发展中起着重要作用。最近，证明了它们与有界格的Ginsberg积是同构的。我的研究目的是推广双边矩阵理论，将其应用于更一般的规划，如具有否定和更多算子的规划。由于否定是由蕴涵符号表示的，所以我引入了部分有序集合中的蕴涵算子作为新积^*的右伴随算子。偏序集是比格更一般的代数系统。在模糊逻辑理论中，乘积算子被称为残差t范数。如果在t范数残馀的偏序集合上加入一些额外的公理，则该代数系统称为格蕴涵代数。我证明了格蕴涵代数与交换有界bck代数是重合的。此外，我还证明了一类具有剩余t范数的有界偏序集合与一类具有条件(S)的有界bck代数在范畴上等价。这一结果意味着我们可以将条件(S)有界bck代数的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.