اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn Forgetting in Tractable Propositional Fragments
100
0
0.0
(
0
)
تأليف
Yisong Wang
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Distilling from a knowledge base only the part that is relevant to a subset of alphabet, which is recognized as forgetting, has attracted extensive interests in AI community. In standard propositional logic, a general algorithm of forgetting and its computation-oriented investigation in various fragments whose satisfiability are tractable are still lacking. The paper aims at filling the gap. After exploring some basic properties of forgetting in propositional logic, we present a resolution-based algorithm of forgetting for CNF fragment, and some complexity results about forgetting in Horn, renamable Horn, q-Horn, Krom, DNF and CNF fragments of propositional logic.
قيم البحث
اقرأ أيضاً
Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design point
s of view, some information content of such property might become irrelevant for the system due to various reasons, e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existing specifications over a given signature. Moreover, in such a scenario, two crucial notions are informative: the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a given property. To address such a scenario in a principled way, we introduce a forgetting-based approach in CTL and show that it can be used to compute SNC and WSC of a property under a given model and over a given signature. We study its theoretical properties and also show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting. Furthermore, we analyse the computational complexity of some basic reasoning tasks for the fragment CTL_AF in particular.
Belief revision is an operation that aims at modifying old be-liefs so that they become consistent with new ones. The issue of belief revision has been studied in various formalisms, in particular, in qualitative algebras (QAs) in which the result is
a disjunction of belief bases that is not necessarily repre-sentable in a QA. This motivates the study of belief revision in formalisms extending QAs, namely, their propositional clo-sures: in such a closure, the result of belief revision belongs to the formalism. Moreover, this makes it possible to define a contraction operator thanks to the Harper identity. Belief revision in the propositional closure of QAs is studied, an al-gorithm for a family of revision operators is designed, and an open-source implementation is made freely available on the web.
Generally intelligent agents exhibit successful behavior across problems in several settings. Endemic in approaches to realize such intelligence in machines is catastrophic forgetting: sequential learning corrupts knowledge obtained earlier in the se
quence, or tasks antagonistically compete for system resources. Methods for obviating catastrophic forgetting have sought to identify and preserve features of the system necessary to solve one problem when learning to solve another, or to enforce modularity such that minimally overlapping sub-functions contain task specific knowledge. While successful, both approaches scale poorly because they require larger architectures as the number of training instances grows, causing different parts of the system to specialize for separate subsets of the data. Here we present a method for addressing catastrophic forgetting called developmental compression. It exploits the mild impacts of developmental mutations to lessen adverse changes to previously-evolved capabilities and `compresses specialized neural networks into a generalized one. In the absence of domain knowledge, developmental compression produces systems that avoid overt specialization, alleviating the need to engineer a bespoke system for every task permutation and suggesting better scalability than existing approaches. We validate this method on a robot control problem and hope to extend this approach to other machine learning domains in the future.
We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagners counting hierarchy, but also th
at the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.
Several variants of the Constraint Satisfaction Problem have been proposed and investigated in the literature for modelling those scenarios where solutions are associated with some given costs. Within these frameworks computing an optimal solution is
an NP-hard problem in general; yet, when restricted over classes of instances whose constraint interactions can be modelled via (nearly-)acyclic graphs, this problem is known to be solvable in polynomial time. In this paper, larger classes of tractable instances are singled out, by discussing solution approaches based on exploiting hypergraph acyclicity and, more generally, structural decomposition methods, such as (hyper)tree decompositions.
الأسئلة المقترحة
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
