Forgetting Based Knowledge Necessary And Sufficient Conditions

Modal logic S5 is an important formalism for epistemic reasoning in agent domain.The Strongest Necessary and Weakest Sufficient Conditions,firstly proposed by Lin in 2001,are important in classical logic.Generally,the strongest necessary condition(SNC)of a proposition is the most general consequence that we can deduce from the proposition under the given theory,and the weakest sufficient condition(WSC)is the most general abduction that we can make from the proposition under the given theory.These two notions are closely related to abduction,definability and forgetting,that play an important role in artificial intelligence.Given the importance of modal logic S5 and the notions of(strongest)necessary condition and(weakest)sufficient condition in the field of artificial intelligence,this paper extends these notions of(strongest)necessary condition and(weakest)sufficient condition from classical logic into S5.In this paper,there are some points are researched: firstly,defining the notions of SNC and WSC under modal logic S5;second,exploring the related properties(Uniqueness,Model-extend,Dual and so on)of those two conditions,and the relationships among SNC,WSC,definability and forgetting.Theoretical demonstration,the SNC(WSC)of a proposition on a set of propositions under a knowledge set is the result of ? {} to forget some irrelevant propositions.Last but not least,in order to compute SNC and WSC,there are two algorithms based on knowledge forgetting,resolution-based and classical forgetting-based,are proposed and implemented,and some experiments are exhibited.Experiments show that resolution-based algorithm is better than that one classical forgetting-based in knowledge forgetting under S5,and the time spent to solve SAT problem has been improved by forgetting some irrelevant knowledge before solving S5 formula.