检索结果-内蒙古大学图书馆

36th International Conference on logic programming (ICLP)

作者： Bellodi, Elena Alberti, Marco Riguzzi, Fabrizio Zese, Riccardo Univ Ferrara Dipartimento Ingn Via Saragat 1 I-44122 Ferrara Italy Univ Ferrara Dipartimento Matemat & Informat Via Saragat 1 I-44122 Ferrara Italy

In Probabilistic logic programming (PLP) the most commonly studied inference task is to compute the marginal probability of a query given a program. In this paper, we consider two other important tasks in the PLP setting: the Maximum-A-Posteriori (MAP) inference task, which determines the most likely values for a subset of the random variables given evidence on other variables, and the Most Probable Explanation (MPE) task, the instance of MAP where the query variables are the complement of the evidence variables. We present a novel algorithm, included in the PITA reasoner, which tackles these tasks by representing each problem as a Binary Decision Diagram and applying a dynamic programming procedure on it. We compare our algorithm with the version of ProbLog that admits annotated disjunctions and can perform MAP and MPE inference. Experiments on several synthetic datasets show that PITA outperforms ProbLog in many cases.

关键词： Probabilistic logics Binary decision diagrams Computer circuits Dynamic programming Inference engines logic programming MAP inferences Marginal probability Maximum a posteriori Most likely Most probable explanation Novel algorithm Query variables Synthetic datasets

来源：评论

学校读者我要写书评

暂无评论

Modular Answer Set programming as a Formal Specification Language

Modular Answer Set Programming as a Formal Specification Lan...

引用

36th International Conference on logic programming (ICLP)

作者： Cabalar, Pedro Fandinno, Jorge Lierler, Yuliya Univ A Coruna La Coruna Spain Univ Potsdam Potsdam Germany Univ Nebraska Omaha Omaha NE USA

In this paper, we study the problem of formal verification for Answer Set programming (ASP), namely, obtaining aformal proofshowing that the answer sets of a given (non-ground) logic programPcorrectly correspond to the solutions to the problem encoded byP, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order)program modulesthat may incorporate local hidden atoms at different levels. Then,verifyingthe logic programPamounts to prove some kind of equivalence betweenPand its modular specification.

关键词： Answer Set programming Formal Specification Formal Verification Modular logic Programs

来源：评论

学校读者我要写书评

暂无评论

Verifying Tight logic Programs with ANTHEM and VAMPIRE

Verifying Tight Logic Programs with ANTHEM and VAMPIRE

引用

36th International Conference on logic programming (ICLP)

作者： Fandinno, Jorge Lifschitz, Vladimir Luehne, Patrick Schaub, Torsten Univ Potsdam Potsdam Germany Univ Texas Austin Austin TX 78712 USA

This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Introduction to the Special Issue On Computational Modelling of Emotion

引用

IEEE TRANSACTIONS ON AFFECTIVE COMPUTING 2021年第2期12卷 277-278页

作者： de Melo, Celso Petters, Dean Parthemore, Joel Moffatt, David Becker-Asano, Christian US Army DEVCOM Res Lab Playa Vista CA 90094 USA Sheffield Hallam Univ Psychol Sheffield S1 1WB S Yorkshire England Univ Shove Dept Cognit Neurosci & Philosophy Mind S-54128 Skovde Sweden Glasgow Caledonian Univ Affect Comp Artificial Intelligence & Serious Gam Glasgow G4 0BA Lanark Scotland Stuttgart Media Univ Artificial Intelligence & Humanrobot Interact HRI D-70569 Stuttgart Germany

The papers in this special issue focus on computational modeling of emotion recognition. Emotions play a pervasive role in personal, social, and professional life. As artificially intelligent systems become pervasive in our lives, it is important that these systems are able to understand emotion in humans and simulate the function of emotion to be effective in their interactions with people. Computational models of emotion contribute towards this goal by, on the one hand, serving as a means to test emotion theories and help understand the function of emotion and, on the other, as the end in itself by simulating appropriate emotion and its downstream consequences – such as expressions of emotion – in computational agents. This special issue presents a critical overview of this cross-disciplinary field, with contributions from some of the leading scholars in cognitive psychology and affective computing, focusing both on theory and practice.

关键词： Special Issues And Sections Computational Modeling Emotion Recognition Affective Computing Probablistic logic Object Recognition programming Robots Intelligent Systems

来源：评论

学校读者我要写书评

暂无评论

Graded Hoare logic and its Categorical Semantics 1

引用

30th European Symposium on programming (ESOP) Held as Part of the 24th European Joint Conferences on theory and practice of Software (ETAPS)

作者： Gaboardi, Marco Katsumata, Shin-ya Orchard, Dominic Sato, Tetsuya Boston Univ Boston MA 02215 USA Natl Inst Informat Tokyo Japan Univ Kent Canterbury Kent England Tokyo Inst Technol Tokyo Japan

ISBN: (数字)9783030720193

ISBN: (纸本)9783030720193;9783030720186

Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of grading, adapted from the world of functional calculi and semantics. We propose Graded Hoare logic (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a graded category which we extend here, introducing graded Freyd categories which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.

关键词： Grading

来源：评论

学校读者我要写书评

暂无评论

Advancing Lazy-Grounding ASP Solving Techniques - Restarts, Phase Saving, Heuristics, and More

引用

theory and practice of logic programming 2020年第5期20卷 609-624页

作者： Weinzierl, Antonius Taupe, Richard Friedrich, Gerhard TU Wien Vienna Univ Technol Vienna Austria Alpen Adria Univ Klagenfurt Austria Siemens AG Osterreich Vienna Austria

Answer-Set programming (ASP) is a powerful and expressive knowledge representation paradigm with a significant number of applications in logic-based AI. The traditional ground-and-solve approach, however, requires ASP programs to be grounded upfront and thus suffers from the so-called grounding bottleneck (i.e., ASP programs easily exhaust all available memory and thus become unsolvable). As a remedy, lazy-grounding ASP solvers have been developed, but many state-of-the-art techniques for grounded ASP solving have not been available to them yet. In this work we present, for the first time, adaptions to the lazy-grounding setting for many important techniques, like restarts, phase saving, domain-independent heuristics, and learned-clause deletion. Furthermore, we investigate their effects and in general observe a large improvement in solving capabilities and also uncover negative effects in certain cases, indicating the need for portfolio solving as known from other solvers.

关键词： Answer-Set programming Lazy-Grounding Solving Techniques Knowledge Representation

来源：评论

学校读者我要写书评

暂无评论

Flexible coinductive logic programming

Flexible coinductive logic programming

引用

36th International Conference on logic programming (ICLP)

作者： DAGNINO, F. R. A. N. C. E. S. C. O. ANCONA, D. A. V. I. D. E. ZUCCA, E. L. E. N. A. Univ Genoa DIBRIS Genoa Italy

Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, calledflexible coinduction, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched bycoclauses, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels.

关键词： coinduction operational semantics declarative semantics soundness completeness

来源：评论

学校读者我要写书评

暂无评论

A First-Order logic with Frames 1

引用

29th European Symposium on programming (ESOP) held as part of the European Joint Conferences on theory and practice of Software (ETAPS)

作者： Murali, Adithya Pena, Lucas Loeding, Christof Madhusudan, P. Univ Illinois Dept Comp Sci Urbana IL 61801 USA Rhein Westfal TH Aachen Dept Comp Sci Aachen Germany

ISBN: (数字)9783030449148

ISBN: (纸本)9783030449148;9783030449131

We propose a novel logic, called Frame logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas- the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.

关键词： Program Verification Program logics Heap Verification First-Order logic First-Order logic with Recursive Definitions

来源：评论

学校读者我要写书评

暂无评论

Incremental maintenance of overgrounded logic programs with tailored simplifications

引用

theory and practice of logic programming 2020年第5期20卷 719-734页

作者： Ianni, Giovambattista Pacenza, Francesco Zangari, Jessica Univ Calabria Dept Math & Comp Sci Arcavacata Di Rende Italy

The repeated execution of reasoning tasks is desirable in many applicative scenarios, such as stream reasoning and event processing. When using answer set programming in such contexts, one can avoid the iterative generation of ground programs thus achieving a significant payoff in terms of computing time. However, this may require some additional amount of memory and/or the manual addition of operational directives in the declarative knowledge base at hand. We introduce a new strategy for generating series of monotonically growing propositional programs. The proposedovergrounded programs with tailoring(OPTs) can be updated and reused in combination with consecutive inputs. With respect to earlier approaches, ourtailored simplificationtechnique reduces the size of instantiated programs. A maintained OPT slowly grows in size from an iteration to another while the update cost decreases, especially in later iterations. In this paper we formally introduce tailored embeddings, a family of equivalence-preserving ground programs which are at the theoretical basis of OPTs and we describe their properties. We then illustrate an OPT update algorithm and report about our implementation and its performance.

关键词： Knowledge Representation and Reasoning Answer Set programming Stream Reasoning Grounding Instantiation of logic Programs Overgrounding

来源：评论

学校读者我要写书评

暂无评论

The External Interface for Extending WASP

引用

theory and practice of logic programming 2020年第2期20卷 225-248页

作者： Dodaro, Carmine Ricca, Francesco Univ Genoa DIBRIS Genoa Italy Univ Calabria DEMACS Arcavacata Di Rende Italy

Answer set programming (ASP) is a successful declarative formalism for knowledge representation and reasoning. The evaluation of ASP programs is nowadays based on the conflict-driven clause learning (CDCL) backtracking search algorithm. Recent work suggested that the performance of CDCL-based implementations can be considerably improved on specific benchmarks by extending their solving capabilities with custom heuristics and propagators. However, embedding such algorithms into existing systems requires expert knowledge of the internals of ASP implementations. The development of effective solver extensions can be made easier by providing suitable programming interfaces. In this paper, we present the interface for extending the CDCL-based ASP solver wasp. The interface is bothgeneral, that is, it can be used for providing either new branching heuristics or propagators, andexternal, that is, the implementation of new algorithms requires no internal modifications of wasp. Moreover, we review the applications of the interface witnessing it can be successfully used to extend wasp for solving effectively hard instances of both real-world and synthetic problems.

关键词： knowledge representation and reasoning answer set programming application programming interface propagators choice heuristics

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：