Reasoning complexity for extended fuzzy description logic with qualifying number restriction

To solve the extended fuzzy description logic with qualifying number restriction （EFALCQ） reasoning problems, EFALCQ is discretely simulated by description logic with qualifying number restriction （ALCQ）, and ALCQ reasoning results are reused to prove the complexity of EFALCQ reasoning problems. The ALCQ simulation method for the consistency of EFALCQ is proposed. This method reduces EFALCQ satisfiability into EFALCQ consistency, and uses EFALCQ satisfiability to discretely simulate EFALCQ satdomain. It is proved that the reasoning complexity for EFALCQ satisfiability, consistency and sat-domain is PSPACE-complete.

New reasoning algorithm based on EFALC

The current extended fuzzy description logics lack reasoning algorithms with TBoxes. The problem of the satisfiability of the extended fuzzy description logic EFALC cut concepts w. r. t. TBoxes is proposed, and a reasoning algorithm is given. This algorithm is designed in the style of tableau algorithms, which is usually used in classical description logics. The transformation rules and the process of this algorithm is described and optimized with three main techniques： recursive procedure call, branch cutting and introducing sets of mesne results. The optimized algorithm is proved sound, complete and with an EXPTime complexity, and the satisfiability problem is EXPTime-complete.

A framework for analysis of extended fuzzy logic

We address a framework for the analysis of extended fuzzy logic(FLe) and elaborate mainly the key characteris-tics of FLe by proving several qualification theorems and proposing a new mathematical tool named the A-granule. Specifically, we reveal that within FLe a solution in the presence of incomplete information approaches the one gained by complete infor-mation. It is also proved that the answers and their validities have a structural isomorphism within the same context. This rela-tionship is then used to prove the representation theorem that addresses the rationality of FLe-based reasoning. As a conse-quence of the developed theoretical description of FLe, we assert that in order to solve a problem, having complete information is not a critical need; however, with more information, the answers achieved become more specific. Furthermore, reasoning based on FLe has the advantage of being computationally less expensive in the analysis of a given problem and is faster.

An Improved Non-Repudiation Protocol and Its Security Analysis

This paper proposes an improved non-repudiation protocol after pointing out two attacks on an existing non-repudiation protocol. To analyze the improved protocol, it also proposes an extension of Kailar logic. Using the extended Kailar logic, the security analysis of the improved prototocol has been presented. Key words non-repudiation protocol - extended Kailar logic - converse assumption procedure CLC number TP 393. 08 Foundation item: Supported by the National Natural Science Foundation of China (90104005) and the Doctoral Science Foundation of Ministry of Education (20020486046)Biography: Li Li(1976-), female, Ph. D candidate, research direction: network security and formal analysis of security protocol.

A proof system of the CaIT calculus

The Internet of Things(IoT)can realize the interconnection of people,machines,and things anytime,anywhere.Most of the existing research mainly focuses on the practical applications of IoT,and there is a lack of research on modeling and reasoning about IoT systems from the perspective of formal methods.Thus,the Calculus of the Internet of Things(CaIT)has been proposed to specify and analyze IoT systems before the actual implementation,which can effectively improve development efficiency,and enhance system quality and reliability.To verify the correctness of IoT systems described by CaIT,this paper presents a proof system for CaIT,in which specifications and verifications are based on the extended Hoare Logic with time.Furthermore,we explore the cooperation between isolated proofs to validate the postconditions of the communication actions occurring in these proofs,with a particular focus on broadcast communication.We also demonstrate the soundness of our proof system.A simple“smart home”is given to illustrate the availability of our proof system.

Extending Hoare Logic with an Infinite While-Rule

In this paper we generalize the while-rule in Hoare calculus to an infinite one and then present a sufficient condition much weaker than the expressiveness for Cook's relative completeness theorem with respect to our new axiomatic system. Using the extended Hoare calculus we can derive true Hoare formulas which contain while- statements free of loop invariants. It is also pointed out that the weak condition is a first order property and therefore provides a possible approach to the characterization of relative completeness which is also a first-order property.

R-Calculus for ELP:An Operational Approach to Knowledge Base Maintenance

Some concepts used in knowledge base maintenance, such as sequence, new law, user's rejection and reconstructions of a knowledge base, are first introduced, and then a framework for extended logic programming (ELP) is given,where an extended logic program is equivalent to a knowledge base. A transition system called R-calculus for ELP is provided. For a given knowledge base and a user's rejection, the Rcalculus for ELP will deduce best revisions of the base. The soundness and the completeness of the Rcalculus for ELP are proved, and the Rcalculus for ELP is implemented in Prolog. In addition, the research is compared with other relevan work.