Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to supp...
详细信息
Epistemic logic Programs (ELPs), extend Answer Set programming (ASP) with epistemic operators. The semantics of such programs is provided in terms of world views, which are sets of belief sets. Different semantic appr...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Epistemic logic Programs (ELPs), extend Answer Set programming (ASP) with epistemic operators. The semantics of such programs is provided in terms of world views, which are sets of belief sets. Different semantic approaches propose different characterizations of world views. Recent work has introduced semantic properties that should be met by any semantics for ELPs, like the Epistemic Splitting Property, that, if satisfied, allows to modularly compute world views in a bottom-up fashion, analogously to 'traditional' ASP. We analyze the possibility to change the perspective, shifting from a bottom-up to a top-down approach to splitting. Our new definition: (i) copes with concerns regarding unfoundedness of world views and subjective constraint monotonicity;(ii) is provably applicable to many of the existing semantics;(iii) operates similarly to "traditional" ASP;(iv) provably coincides with the bottom-up notion of splitting at least on the class of Epistemically Stratified Programs (which are, intuitively, those where the use of epistemic operators is stratified).
The interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false a...
详细信息
ISBN:
(数字)9783031300448
ISBN:
(纸本)9783031300431;9783031300448
The interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false alarms may arise. An ideal, but uncommon, situation is completeness of the abstraction that can ensure no false alarm is introduced by the abstract interpreter. Local Completeness logic is a proof system that can decide both correctness and incorrectness of a program: any provable triple proves(A) [P] c [Q] in the logic implies completeness of an intensional abstraction of program c on input P and is such that Q can be used to decide (in)correctness. However, completeness itself is an extensional property of the function computed by the program, while the above intensional analysis depends on the way the program is written and therefore not all valid triples can be derived in the proof system. Our main contribution is the study of new inference rules which allow one to perform part of the intensional analysis in a more precise abstract domain, and then to transfer the result back to the coarser domain. With these new rules, all (extensionally) valid triples can be derived in the proof system, thus untying the set of provable properties from the way the program is written.
We propose a method for computing supported models of normal logic programs in vector spaces using gradient information. First, the program is translated into a definite program and embedded into a matrix representing...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
We propose a method for computing supported models of normal logic programs in vector spaces using gradient information. First, the program is translated into a definite program and embedded into a matrix representing the program. We introduce a loss function based on the implementation of the immediate consequence operator T-P by matrix-vector multiplication with a suitable thresholding function, and we incorporate regularization terms into the loss function to avoid undesirable results. The proposed thresholding operation is an almost everywhere differentiable alternative to the non-linear thresholding operation. We report the results of several experiments where our method shows promising performance when used with adaptive gradient update.
Concurrent randomized programs in the oblivious adversary model are extremely difficult for modular verification because the interaction between threads is very sensitive to the program structure and the exe...
详细信息
Probabilistic logic Programs under the distribution semantics (PLPDS) do not allow statistical probabilistic statements of the form "90% of birds fly", which were defined "Type 1" statements by Hal...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Probabilistic logic Programs under the distribution semantics (PLPDS) do not allow statistical probabilistic statements of the form "90% of birds fly", which were defined "Type 1" statements by Halpern. In this paper, we add this kind of statements to PLPDS and introduce the PASTA ("Probabilistic Answer set programming for STAtistical probabilities") language. We translate programs in our new formalism into probabilistic answer set programs under the credal semantics. This approach differs from previous proposals, such as the one based on "probabilistic conditionals" as, instead of choosing a single model by making the maximum entropy assumption, we take into consideration all models and we assign probability intervals to queries. In this way we refrain from making assumptions and we obtain a more neutral framework. We also propose an inference algorithm and compare it with an existing solver for probabilistic answer set programs on a number of programs of increasing size, showing that our solution is faster and can deal with larger instances.
SHACL is a W3C-proposed language for expressing structural constraints on RDF graphs. In recent years, SHACL's popularity has risen quickly. This rise in popularity comes with questions related to its place in the...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
SHACL is a W3C-proposed language for expressing structural constraints on RDF graphs. In recent years, SHACL's popularity has risen quickly. This rise in popularity comes with questions related to its place in the semantic web, particularly about its relation to OWL (the de facto standard for expressing ontological information on the web) and description logics (which form the formal foundations of OWL). We answer these questions by arguing that SHACL is in fact a description logic. On the one hand, our answer is surprisingly simple, some might even say obvious. But, on the other hand, our answer is also controversial. By resolving this issue once and for all, we establish the field of description logics as the solid formal foundations of SHACL.
This paper introduces formal models for emotional reasoning, expressing emotional states and emotional causality, using action reasoning and transition systems. A general framework is defined, comprised of two main co...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
This paper introduces formal models for emotional reasoning, expressing emotional states and emotional causality, using action reasoning and transition systems. A general framework is defined, comprised of two main components: 1) a model for emotions based on the Appraisal theory of Emotion (AE), and 2) a model for emotional change based on Hedonic Emotion Regulation (HER). A particular transition system is modelled in which states correspond to human emotional states and transitions correspond to restrictive (safe) ways to influence emotions while reducing negative emotional side-effects. The introduced emotional reasoning can be applied to guide a software agent's actions for dealing with emotions while estimating and planning future interactions with humans.
Technological progress in Answer Set programming (ASP) has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in nonmonotonic reasoning, efforts have also been mad...
详细信息
Technological progress in Answer Set programming (ASP) has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in nonmonotonic reasoning, efforts have also been made to reconcile ASP with classical first-order (FO) logic. This has resulted in the development of FO(.), an expressive extension of FO, which allows ASP-like problem solving in a purely classical setting. This language may be more accessible to domain experts already familiar with FO and may be easier to combine with other formalisms that are based on classical logic. It is supported by the IDP inference system, which has successfully competed in a number of ASP competitions. Here, however, technological progress has been hampered by the limited number of systems that are available for FO(.). In this paper, we aim to address this gap by means of a translation tool that transforms an FO(.) specification into ASP-Core-2, thereby allowing ASP-Core-2 solvers to be used as solvers for FO(.) as well. We present experimental results to show that the resulting combination of our translation with an off-the-shelf ASP solver is competitive with the IDP system as a way of solving problems formulated in FO(.).
暂无评论