This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS mor...This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS more difficult tostudy. This is in part because of a failure of EI-CTRS to guarantee that thereexist least Herbrand models in classical logical point of views. The key idea ofEI-model is to explain that 't ≠ s' means that the two concepts representedby t and s respectively actually belong to distinguished basic concepts repre-sented by two constructor-ground terms. We define the concept of EI-model,and show that there exist least Herbrand ELmodels for EI-satisfiable EI-CTRS.From algebraic and logic point of view, we show that there are very strong rea-sons for regarding the least Herbrand EI-models as the intended semantics ofEI-CTRS. According to fixpoint theory, we develop a method to construct leastHerbrand EI-models in a bottom-up manner. Moreover, we discuss soundnessand completeness of EI-rewrite for EI-model semantics.展开更多
The development of the object-oriented paradigm has suffered from the lackof any generally accepted formal foundations for its semantic definition. Toaddress this issue, we propose the development of the logic-based s...The development of the object-oriented paradigm has suffered from the lackof any generally accepted formal foundations for its semantic definition. Toaddress this issue, we propose the development of the logic-based semantics ofthe object-oriented paradigm. By combining the logic- with the object-orientedparadigm of computing first, this paper discusses formally the semantics of aquite purely object-oriented logic paradigm in terms of proof theory modeltheory and Aspoint theory from the viewpoint of logic. The operational anddeclarative semantics is given. And then the correspondence between soundnessand completeness has been discussed formally.展开更多
Tree logic, inherited from ambient logic, is introduced as the formal foundation of related programming language and type systems, In this paper, we introduce recursion into such logic system, which can describe the t...Tree logic, inherited from ambient logic, is introduced as the formal foundation of related programming language and type systems, In this paper, we introduce recursion into such logic system, which can describe the tree data more dearly and concisely. By making a distinction between proposition and predicate, a concise semantics interpretation for our modal logic is given. We also develop a model checking algorithm for the logic without △ operator. The correctness of the algorithm is shown. Such work can be seen as the basis of the semi-structured data processing language and more flexible type system.展开更多
We give two generalizations of Tarski’s fixpoint theorem in the setting of residuated lattices and use them to establish van Emdem-Kowalski’s least fixpoint semantics for residuated lattice-valued logic programs.
The famous diagonal argument plays a prominent role in set the ory as well as in the proof of undecidability results in computability the ory and incompleteness results in metamathematics.Lawvere(1969)brings to light ...The famous diagonal argument plays a prominent role in set the ory as well as in the proof of undecidability results in computability the ory and incompleteness results in metamathematics.Lawvere(1969)brings to light the common schema among them through a pretty neat fixpoint the orem which generalizes the diagonal argument behind Cantor's theorem and characterizes self-reference explicitly in category theory.Not until Yanofsky(2003)rephrases Lawvere’s fixpoint theorem using sets and functions,Lawvere's work has been overlooked by logicians.This paper will continue Yanofsky's work,and show more applications of Lawvere's fixpoint theorem to demonstrate the ubiquity of the theorem.For example,this paper will use it to construct uncomputable real number,unnameable real number,partial re cursive but not potentially recursive function,Berry paradox,and fast growing Busy Beaver function.Many interesting lambda fixpoint combinators can also be fitted into this schema.Both Curry's Y combinator and Turing's combinator follow from Lawvere's theorem,as well as their call-by-value versions.At last,it can be shown that the lambda calculus version of the fixpoint lemma also fits Lawvere’s schema.展开更多
分析了描述逻辑循环术语集的研究现状和存在的问题,在F.Baader工作的基础上进一步研究了描述逻辑εL混合循环术语集的LCS(least common subsumer)和MSC(most specific concept)推理问题.给出了εL混合循环术语集的语法和语义.针对εL混...分析了描述逻辑循环术语集的研究现状和存在的问题,在F.Baader工作的基础上进一步研究了描述逻辑εL混合循环术语集的LCS(least common subsumer)和MSC(most specific concept)推理问题.给出了εL混合循环术语集的语法和语义.针对εL混合循环术语集LCS和MSC推理的需要,提出了TBox-完全的概念,并重新定义了描述图.使用描述图和TBox-完全给出了最大不动点语义下εL混合循环术语集LCS和MSC的推理算法,证明了推理算法的正确性,并证明了推理算法是多项式时间复杂的.该推理算法为εL混合循环术语集的LCS和MSC推理提供了理论基础.展开更多
文摘This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS more difficult tostudy. This is in part because of a failure of EI-CTRS to guarantee that thereexist least Herbrand models in classical logical point of views. The key idea ofEI-model is to explain that 't ≠ s' means that the two concepts representedby t and s respectively actually belong to distinguished basic concepts repre-sented by two constructor-ground terms. We define the concept of EI-model,and show that there exist least Herbrand ELmodels for EI-satisfiable EI-CTRS.From algebraic and logic point of view, we show that there are very strong rea-sons for regarding the least Herbrand EI-models as the intended semantics ofEI-CTRS. According to fixpoint theory, we develop a method to construct leastHerbrand EI-models in a bottom-up manner. Moreover, we discuss soundnessand completeness of EI-rewrite for EI-model semantics.
文摘The development of the object-oriented paradigm has suffered from the lackof any generally accepted formal foundations for its semantic definition. Toaddress this issue, we propose the development of the logic-based semantics ofthe object-oriented paradigm. By combining the logic- with the object-orientedparadigm of computing first, this paper discusses formally the semantics of aquite purely object-oriented logic paradigm in terms of proof theory modeltheory and Aspoint theory from the viewpoint of logic. The operational anddeclarative semantics is given. And then the correspondence between soundnessand completeness has been discussed formally.
基金Supported by the National Natural Sciences Foun-dation of China (60233010 ,60273034 ,60403014) ,863 ProgramofChina (2002AA116010) ,973 Programof China (2002CB312002)
文摘Tree logic, inherited from ambient logic, is introduced as the formal foundation of related programming language and type systems, In this paper, we introduce recursion into such logic system, which can describe the tree data more dearly and concisely. By making a distinction between proposition and predicate, a concise semantics interpretation for our modal logic is given. We also develop a model checking algorithm for the logic without △ operator. The correctness of the algorithm is shown. Such work can be seen as the basis of the semi-structured data processing language and more flexible type system.
文摘We give two generalizations of Tarski’s fixpoint theorem in the setting of residuated lattices and use them to establish van Emdem-Kowalski’s least fixpoint semantics for residuated lattice-valued logic programs.
文摘The famous diagonal argument plays a prominent role in set the ory as well as in the proof of undecidability results in computability the ory and incompleteness results in metamathematics.Lawvere(1969)brings to light the common schema among them through a pretty neat fixpoint the orem which generalizes the diagonal argument behind Cantor's theorem and characterizes self-reference explicitly in category theory.Not until Yanofsky(2003)rephrases Lawvere’s fixpoint theorem using sets and functions,Lawvere's work has been overlooked by logicians.This paper will continue Yanofsky's work,and show more applications of Lawvere's fixpoint theorem to demonstrate the ubiquity of the theorem.For example,this paper will use it to construct uncomputable real number,unnameable real number,partial re cursive but not potentially recursive function,Berry paradox,and fast growing Busy Beaver function.Many interesting lambda fixpoint combinators can also be fitted into this schema.Both Curry's Y combinator and Turing's combinator follow from Lawvere's theorem,as well as their call-by-value versions.At last,it can be shown that the lambda calculus version of the fixpoint lemma also fits Lawvere’s schema.
文摘分析了描述逻辑循环术语集的研究现状和存在的问题,在F.Baader工作的基础上进一步研究了描述逻辑εL混合循环术语集的LCS(least common subsumer)和MSC(most specific concept)推理问题.给出了εL混合循环术语集的语法和语义.针对εL混合循环术语集LCS和MSC推理的需要,提出了TBox-完全的概念,并重新定义了描述图.使用描述图和TBox-完全给出了最大不动点语义下εL混合循环术语集LCS和MSC的推理算法,证明了推理算法的正确性,并证明了推理算法是多项式时间复杂的.该推理算法为εL混合循环术语集的LCS和MSC推理提供了理论基础.
