Przymusinski extended the notion of stratified logic programs,developed by Apt,Blair and Walker,and by van Gelder,to stratified databases that allow both negative premises and disjunctive consequents.However,he did no...Przymusinski extended the notion of stratified logic programs,developed by Apt,Blair and Walker,and by van Gelder,to stratified databases that allow both negative premises and disjunctive consequents.However,he did not provide a fixpoint theory for such class of databases.On the other hand,although a fixpoint semantics has been developed by Minker and Rajasekar for non-Horn logic programs,it is tantamount to traditional minimal model semantics which is not sufficient to capture the intended meaning of negation in the premises of clauses in stratified databases.In this paper,a fixpoint approach to stratified databases is developed,which corresponds with the perfect model semantics. Moreover,algorithms are proposed for computing the set of perfect models of a stratified database.展开更多
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推理提供了理论基础.展开更多
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.展开更多
文摘Przymusinski extended the notion of stratified logic programs,developed by Apt,Blair and Walker,and by van Gelder,to stratified databases that allow both negative premises and disjunctive consequents.However,he did not provide a fixpoint theory for such class of databases.On the other hand,although a fixpoint semantics has been developed by Minker and Rajasekar for non-Horn logic programs,it is tantamount to traditional minimal model semantics which is not sufficient to capture the intended meaning of negation in the premises of clauses in stratified databases.In this paper,a fixpoint approach to stratified databases is developed,which corresponds with the perfect model semantics. Moreover,algorithms are proposed for computing the set of perfect models of a stratified database.
文摘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推理提供了理论基础.
基金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.
