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

Verifiable Certificates for Predicate Subtyping 28th

Verifiable Certificates for Predicate Subtyping

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

作者： Gilbert, Frederic INRIA Cachan France

ISBN: (纸本)9783030171841;9783030171834

Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a solution to this issue with a minimal formalization of predicate subtyping, named PVS-Core, together with a system of verifiable certificates for PVS-Core, named PVS-Cert. PVS-Cert is based on the introduction of proof terms and explicit coercions. Its design is similar to that of PTSs with dependent pairs, with the exception of the definition of conversion, which is based on a specific notion of reduction -> (beta*), corresponding to beta-reduction combined with the erasure of coercions. The use of this reduction instead of the more standard reduction -> (beta sigma) allows to establish a simple correspondence between PVS-Core and PVS-Cert. On the other hand, a type-checking algorithm is designed for PVS-Cert, built on proofs of type preservation of -> (beta sigma) and strong normalization of both -> (beta sigma) and -> (beta*). Combining these results, PVS-Cert judgements are used as verifiable certificates for predicate subtyping. In addition, the reduction -> (beta sigma) is used to define a cut elimination procedure for predicate subtyping. This definition provides a new tool to study the properties of predicate subtyping, as illustrated with a proof of consistency.

关键词： Higher-order logic Predicate subtyping Type theory Proof theory

来源：评论

学校读者我要写书评

暂无评论

Answer Set programming 1st ed. 2019

引用

2019年

作者： Vladimir Lifschitz

ISBN: (数字)9783030246587

ISBN: (纸本)9783030246570

Answer set programming (ASP) is a programming methodology oriented towards combinatorial search problems. In such a problem, the goal is to find a solution among a large but finite number of possibilities. The idea of ASP came from research on artificial intelligence and computational logic. ASP is a form of declarative programming: an ASP program describes what is counted as a solution to the problem, but does not specify an algorithm for solving it. Search is performed by sophisticated software systems called answer set solvers. Combinatorial search problems often arise in science and technology, and ASP has found applications in diverse areas―in historical linguistic, in bioinformatics, in robotics, in space exploration, in oil and gas industry, and many others. The importance of this programming method was recognized by the Association for the Advancement of Artificial Intelligence in 2016, when AI Magazine published a special issue on answer set programming. The book will introduce the reader to the theory and practice of ASP. It will describe the input language of the answer set solver CLINGO, which was designed at the University of Potsdam in Germany and is used today by ASP programmers in many countries. It will include numerous examples of ASP programs and present the mathematical theory that ASP is based on. There will be many exercises with complete solutions.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Founded World Views with Autoepistemic Equilibrium logic 15th

Founded World Views with Autoepistemic Equilibrium Logic

引用

15th International Conference on logic programming and Nonmonotonic Reasoning (LPNMR)

作者： Cabalar, Pedro Fandinno, Jorge del Cerro Luis, Farinas Univ A Coruna La Coruna Spain Univ Toulouse CNRS IRIT Toulouse France

ISBN: (纸本)9783030205287;9783030205270

Defined by Gelfond in 1991 (G91), epistemic specifications (or programs) are an extension of logic programming under stable models semantics that introduces subjective literals. A subjective literal allows checking whether some regular literal is true in all (or in some of) the stable models of the program, being those models collected in a set called world view. One epistemic program may yield several world views but, under the original G91 semantics, some of them resulted from self-supported derivations. During the last eight years, several alternative approaches have been proposed to get rid of these self-supported world views. Unfortunately, their success could only be measured by studying their behaviour on a set of common examples in the literature, since no formal property of "self-supportedness" had been defined. To fill this gap, we extend in this paper the idea of unfounded set from standard logic programming to the epistemic case. We define when a world view is founded with respect to some program and propose the foundedness property for any semantics whose world views are always founded. Using counterexamples, we explain that the previous approaches violate foundedness, and proceed to propose a new semantics based on a combination of Moore's Autoepistemic logic and Pearce's Equilibrium logic. The main result proves that this new semantics precisely captures the set of founded G91 world views.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Conflict-driven Inductive logic programming

arXiv

引用

arXiv 2020年

作者： Law, Mark ILASP Limited United Kingdom

The goal of Inductive logic programming (ILP) is to learn a program that explains a set of examples. Until recently, most research on ILP targeted learning Prolog programs. The ILASP system instead learns Answer Set Programs (ASP). Learning such expressive programs widens the applicability of ILP considerably;for example, enabling preference learning, learning common-sense knowledge, including defaults and exceptions, and learning non-deterministic theories. Early versions of ILASP can be considered meta-level ILP approaches, which encode a learning task as a logic program and delegate the search to an ASP solver. More recently, ILASP has shifted towards a new method, inspired by conflict-driven SAT and ASP solvers. The fundamental idea of the approach, called Conflict-driven ILP (CDILP), is to iteratively interleave the search for a hypothesis with the generation of constraints which explain why the current hypothesis does not cover a particular example. These coverage constraints allow ILASP to rule out not just the current hypothesis, but an entire class of hypotheses that do not satisfy the coverage constraint. This paper formalises the CDILP approach and presents the ILASP3 and ILASP4 systems for CDILP, which are demonstrated to be more scalable than previous ILASP systems, particularly in the presence of noise. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2020, The Authors. All rights reserved.

关键词： Inductive logic programming (ILP)

来源：评论

学校读者我要写书评

暂无评论

Knowledge representation analysis of graph mining

引用

ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE 2019年第1-3期86卷 21-60页

作者： van der Hallen, Matthias Paramonov, Sergey Janssens, Gerda Denecker, Marc Katholieke Univ Leuven Dept Comp Sci Celestijnenlaan 200ABox 2402 B-3001 Leuven Belgium

This paper analyses the graph mining problem, and the frequent pattern mining task associated with it. In general, frequent pattern mining looks for a graph which occurs frequently within a network or, in the transactional setting, within a dataset of graphs. We discuss this task in the transactional setting, which is a problem of interest in many fields such as bioinformatics, chemoinformatics and social networks. We look at the graph mining problem from a Knowledge Representation point of view, hoping to learn something about support for higher-order logics in declarative languages and solvers. Graph mining is studied as a prototypical problem;it is easily expressible mathematically and exists in many variations. As such, it appears to be a prime candidate for a declarative approach;one would expect this allows for a clear, structured, statement of the problem combined with easy adaptation to changing requirements and variations. Current state-of-the-art KR languages such as IDP and ASP aspire to be practical solvers for such problems (Bruynooghe, theory practice logic Program. (TPLP) 15(6), 783-817 2015). Nevertheless, expressing the graph mining problem in these languages requires unexpectedly complicated and unintuitive encoding techniques. These techniques are in contrast to the ease with which one can transform the mathematical definition of graph mining to a higher-order logic specification, and distract from the problem essentials, complicating possible future adaptation. In this paper, we argue that efforts should be made towards supporting higher-order logic specifications in modern specification languages, without unintuitive and complicated encoding techniques. We argue that this not only makes representation clearer and more susceptible to future adaptation, but might also allow for faster, more competitive solver techniques to be implemented.

关键词： Knowledge representation Higher order Graph mining Answer set programming Imperative declarative programming

来源：评论

学校读者我要写书评

暂无评论

A FUZZY logic-BASED MACHINE LEARNING ALGORITHM FOR PRODUCT DISTRIBUTION IN SUPPLY CHAINS CONSIDERING RIVAL'S STRATEGIC DECISIONS

引用

INTERNATIONAL JOURNAL OF INDUSTRIAL ENGINEERING-theory APPLICATIONS AND practice 2020年第6期27卷 933-958页

作者： Delgoshaei, Aidin MohammadAzari, Maryam Hanjani, Sepehr Esmaeili Fard, Forough Beigizadeh, Razieh Aram, Aisa Khoshniat Ryerson Univ Dept Mech & Ind Engn Toronto ON Canada Islamic Azad Univ Fac Engn Karaj Branch Alborz Iran Univ Putra Malaysia Dept Mech & Mfg Engn Serdang Malaysia Islamic Azad Univ Rasht Branch Dept Management Guilan Iran Social Sci Univ Ankara Fac Social Sci & Humanities Ankara Turkey

A new fuzzy-based machine learning method is addressed in this research to respond to rival's strategy. This method aims to find the best production and product distribution strategy while rivals can take various market strategies that affect a market quota. A multi-period mixed-integer programming method is developed for scheduling a supply chain over a time horizon. The developed model is flexible enough to use in industries. To solve the problem, we developed a hybrid fuzzy-based multi-layer perceptron and simulated annealing algorithm. Its results are compared with branch and bound, hybrid Tabu Search and Simulated Annealing algorithms, hybrid ant colony optimization, and simulated annealing algorithms. A new measuring index is developed to evaluate the production strategies in dynamic market demands. The outcomes reveal that while product demands are considered stochastic, it may affect the market quota among suppliers. Comparing different game theories shows that the proposed method can successfully generate effective production strategies while rivals change their approach.

关键词： supply chain management fuzzy logic game theory machine learning multi-layer perceptron

来源：评论

学校读者我要写书评

暂无评论

Internet Routing and Non-monotonic Reasoning 15th

Internet Routing and Non-monotonic Reasoning

引用

15th International Conference on logic programming and Nonmonotonic Reasoning (LPNMR)

作者： Wang, Anduo Chen, Zhijia Temple Univ Philadelphia PA 19122 USA

ISBN: (纸本)9783030205287;9783030205270

Internet routing is the process of selecting paths across the Internet to connect the communicating hosts, it is unique in that path selection is jointly determined by a network of independently operated networks, known as domains or Autonomous Systems (ASes), that interconnect to form the Internet. In fact, the present routing infrastructure takes such an extreme position that it favors local autonomy-an AS can use arbitrary path preference to override the default shortest path policy, at the expense of potential global oscillation-a collection of AS preferences (policies) can fail to converge on a stable path, a path that is also the most preferred possible for every AS along the path. In this paper, we examine the route oscillation problem with non-monotonic reasoning. We observe that, in the absence of any AS specific policies, Internet routing degenerates into the monotonic computation of shortest path-a preferred (shorter) (super)path always extends another preferred (sub)path;But fully autonomous AS policies are non-monotonic a path favored by one AS can be an extension of a less preferred path of a neighbor, to which an "upgrade" to a better path can cause this AS to downgrade to a less preferred path previously discarded. Based on this insight, we present an Answer Set programming (ASP) formulation that allows for automatic oscillation detection. Our evaluation using the clingo ASP solver is promising: on realistic Internet topology and representative policies, clingo can detect anomalies within 35 s.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

C-ASP: Continuous ASP-Based Reasoning over RDF Streams 15th

C-ASP: Continuous ASP-Based Reasoning over RDF Streams

引用

15th International Conference on logic programming and Nonmonotonic Reasoning (LPNMR)

作者： Pham, Thu-Le Ali, Muhammad Intizar Mileo, Alessandra Natl Univ Ireland Insight Ctr Data Analyt Galway Ireland IDA Bussiness Pk Galway Ireland Dublin City Univ Insight Ctr Data Analyt Dublin 9 Ireland

ISBN: (纸本)9783030205287;9783030205270

The ability to perform complex reasoning over data streams has recently become an important area of research in the Semantic Web community. Most of SPARQL-inspired engines have limitations in capturing sophisticated user requirements and dealing with complex reasoning tasks. To address these challenges, we propose and implement C-ASP, a reasoning system based on the Answer Set programming (ASP) system Clingo and extended to handle continuous reasoning requests over RDF streams. We provide the syntax of the C-ASP language, as well as a set of examples in order to illustrate its expressive power. In addition, we present preliminary experimental results showing C-ASP performances.

关键词： Stream reasoning Answer Set programming Semantic Web RDF

来源：评论

学校读者我要写书评

暂无评论

Splitting Epistemic logic Programs 15th

Splitting Epistemic Logic Programs

引用

15th International Conference on logic programming and Nonmonotonic Reasoning (LPNMR)

作者： Cabalar, Pedro Fandinno, Jorge Farinas del Cerro, Luis Univ A Coruna Corunna Spain Univ Toulouse CNRS IRIT Toulouse France

ISBN: (纸本)9783030205287;9783030205270

Epistemic logic programs constitute an extension of the stable models semantics to deal with new constructs called subjective literals. Informally speaking, a subjective literal allows checking whether some regular literal is true in all or some stable models. As it can be imagined, the associated semantics has proved to be non-trivial, as the truth of subjective literals may interfere with the set of stable models it is supposed to query. As a consequence, no clear agreement has been reached and different semantic proposals have been made in the literature. Unfortunately, comparison among these proposals has been limited to a study of their effect on individual examples, rather than identifying general properties to be checked. In this paper, we propose an extension of the well-known splitting property for logic programs to the epistemic case. We formally define when an arbitrary semantics satisfies the epistemic splitting property and examine some of the consequences that can be derived from that, including its relation to conformant planning and to epistemic constraints. Interestingly, we prove (through counterexamples) that most of the existing proposals fail to fulfill the epistemic splitting property, except the original semantics proposed by Gelfond in 1991.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Omission-based Abstraction for Answer Set Programs∗

arXiv

引用

arXiv 2020年

作者： Saribatur, Zeynep G. Eiter, Thomas Institute of Logic and Computation TU Wien Vienna Austria

ion is a well-known approach to simplify a complex problem by over-approximating it with a deliberate loss of information. It was not considered so far in Answer Set programming (ASP), a convenient tool for problem solving. We introduce a method to automatically abstract ASP programs that preserves their structure by reducing the vocabulary while ensuring an over-approximation (i.e., each original answer set maps to some abstract answer set). This allows for generating partial answer set candidates that can help with approximation of reasoning. Computing the abstract answer sets is intuitively easier due to a smaller search space, at the cost of encountering spurious answer sets. Faithful (non-spurious) abstractions may be used to represent projected answer sets and to guide solvers in answer set construction. For dealing with spurious answer sets, we employ an ASP debugging approach to help with abstraction refinement, which determines atoms as badly omitted and adds them back in the abstraction. As a show case, we apply abstraction to explain unsatisfiability of ASP programs in terms of blocker sets, which are the sets of atoms such that abstraction to them preserves unsatisfiability. Their usefulness is demonstrated by experimental results. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2020, The Authors. All rights reserved.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：