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

34th International Conference on logic programming (ICLP)

作者： Cabalar, Pedro Fadinno, Jorge Del Cerro, Luis Farinas Pearce, David Univ A Coruna Dept Comp Sci Corunna Spain Univ Toulouse CNRS IRIT Toulouse France Univ Politecn Madrid Madrid Spain

In this paper, we propose a variant of Answer Set programming (ASP) with evaluable functions that extends their application to sets of objects, something that allows a fully logical treatment of aggregates. Formally, we start from the syntax of First Order logic with equality and the semantics of Quantified Equilibrium logic with evaluable functions (QEL(F)(=)). Then, we proceed to incorporate a new kind of logical term, intensional set (a construct commonly used to denote the set of objects characterised by a given formula), and to extend QEL(F)(=) semantics for this new type of expression. In our extended approach, intensional sets can be arbitrarily used as predicate or function arguments or even nested inside other intensional sets, just as regular first-order logical terms. As a result, aggregates can be naturally formed by the application of some evaluable function (count, sum, maximum, etc) to a set of objects expressed as an intensional set. This approach has several advantages. First, while other semantics for aggregates depend on some syntactic transformation (either via a reduct or a formula translation), the QEL(F)(=) interpretation treats them as regular evaluable functions, providing a compositional semantics and avoiding any kind of syntactic restriction. Second, aggregates can be explicitly defined now within the logical language by the simple addition of formulas that fix their meaning in terms of multiple applications of some (commutative and associative) binary operation. For instance, we can use recursive rules to define sum in terms of integer addition. Last, but not least, we prove that the semantics we obtain for aggregates coincides with the one defined by Gelfond and Zhang for the Alog language, when we restrict to that syntactic fragment.

关键词： Answer Set programming Equilibrium logic Partial Functions Aggregates

来源：评论

学校读者我要写书评

暂无评论

An integer programming formulation for the music school timetabling problem 12

An integer programming formulation for the music school time...

引用

12th International Conference on the practice and theory of Automated Timetabling, PATAT 2018

作者： Ásgeirsson, E.I. Gunnarsdóttir, P. School of Science and Engineering ICE-TCS Reykjavik University Iceland School of Science and Engineering Reykjavik University Iceland

ISBN: (纸本)9780992998424

Research on educational timetabling has focused mostly on highschool timetabling, university timetabling and examination timetabling. We introduce a new problem, the music school timetabling problem which is a hybrid between the high-school and university timetabling problems, sharing many features from both problems. The music school timetabling problem contains both group courses and private lessons that must be scheduled, with limitations on the availability of both teachers and students. We give an integer programming formulation for the music school timetabling problem and present the results from a case study from Tónmenntaskóli Reykjavíkur, a music school in Reykjavík, Iceland. The results show that, although the problem is challenging, we can still get high quality timetables using a two-phased approach, where we focus first on group courses at the music school, before scheduling private lessons. © PATAT 2018 Organizing Committee.

关键词： Integer programming

来源：评论

学校读者我要写书评

暂无评论

Ontoscene, a logic-based scene interpreter: Implementation and application in the rock art domain

arXiv

引用

arXiv 2019年

作者： BRIOLA, DANIELA MASCARDI, VIVIANA GIOSEFFI, MASSIMILIANO Department of Computer Sciences Systems and Communications University of Milano Bicocca Italy Department of Informatics Bioengineering Robotics and Systems Engineering University of Genova Italy

We present OntoScene, a framework aimed at understanding the semantics of visual scenes starting from the semantics of their elements and the spatial relations holding between them. OntoScene exploits ontologies for representing knowledge and Prolog for specifying the interpretation rules that domain experts may adopt, and for implementing the SceneInterpreter engine. Ontologies allow the designer to formalize the domain in a reusable way, and make the system modular and interoperable with existing multiagent systems, while Prolog provides a solid basis to define complex rules of interpretation in a way that can be affordable even for people with no background in Computational logics. The domain selected for experimenting OntoScene is that of prehistoric rock art, which provides us with a fascinating and challenging testbed. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2019, The Authors. All rights reserved.

关键词： Ontology

来源：评论

学校读者我要写书评

暂无评论

Routing Driverless Transport Vehicles in Car Assembly with Answer Set programming

Routing Driverless Transport Vehicles in Car Assembly with A...

引用

34th International Conference on logic programming (ICLP)

作者： Gebser, Martin Obermeier, Philipp Schaub, Torsten Ratsch-Heitmann, Michel Runge, Mario Univ Potsdam Potsdam Germany Mercedes Benz Ludwigsfelde GmbH Ludwigsfelde Germany

Automated storage and retrieval systems are principal components of modern production and warehouse facilities. In particular, automated guided vehicles nowadays substitute human-operated pallet trucks in transporting production materials between storage locations and assembly stations. While low-level control systems take care of navigating such driverless vehicles along programmed routes and avoid collisions even under unforeseen circumstances, in the common case of multiple vehicles sharing the same operation area, the problem remains how to set up routes such that a collection of transport tasks is accomplished most effectively. We address this prevalent problem in the context of car assembly at Mercedes-Benz Ludwigsfelde GmbH, a large-scale producer of commercial vehicles, where routes for automated guided vehicles used in the production process have traditionally been hand-coded by human engineers. Such adhoc methods may suffice as long as a running production process remains in place, while any change in the factory layout or production targets necessitates tedious manual reconfiguration, not to mention the missing portability between different production plants. Unlike this, we propose a declarative approach based on Answer Set programming to optimize the routes taken by automated guided vehicles for accomplishing transport tasks. The advantages include a transparent and executable problem formalization, provable optimality of routes relative to objective criteria, as well as elaboration tolerance towards particular factory layouts and production targets. Moreover, we demonstrate that our approach is efficient enough to deal with the transport tasks evolving in realistic production processes at the car factory of Mercedes-Benz Ludwigsfelde GmbH.

关键词： automated guided vehicle routing car assembly operations answer set programming

来源：评论

学校读者我要写书评

暂无评论

An A∗ algorithm for solving a prize-collecting sequencing problem with one common and multiple secondary resources and time windows 12

An A∗ algorithm for solving a prize-collecting sequencing p...

引用

12th International Conference on the practice and theory of Automated Timetabling, PATAT 2018

作者： Horn, Matthias Raidl, Günther R. Rönnberg, Elina Institute of Logic and Computation TU Wien Austria Department of Mathematics Linköping University Sweden

ISBN: (纸本)9780992998424

In the considered sequencing problem, a subset of a given set of jobs is to the be scheduled. A scheduled job has to execute without preemption and during this time, the job needs both a common resource for a part of the execution as well as a secondary resource for the whole execution time. The common resource is shared by all jobs while a secondary resource is shared only by a subset of the jobs. Each job has one or more time windows and due to these, it may not be possible to schedule all jobs. Instead, each job is associated with a prize and the task is to select a subset of jobs which yields a feasible schedule with a maximum total sum of prizes. First, we argue that the problem is NP-hard. Then, we present an exact A∗ algorithm and derive different upper bounds for the total prize;these bounds are based on constraint and Lagrangian relaxations of a linear programming relaxation of a multidimensional knapsack problem. For comparison, a compact mixed integer programming (MIP) model and a constraint programming model are also presented. An extensive experimental evaluation on two types of problem instances shows that the A∗ algorithm outperforms the other approaches and is able to solve small to medium size instances with up to about 50 jobs to proven optimality. In cases where A∗ does not prove that an optimal solution is found, the obtained upper bounds are stronger than those of the MIP model. © PATAT 2018 Organizing Committee.

关键词： Integer programming

来源：评论

学校读者我要写书评

暂无评论

PATAT 2018 - Proceedings of the 12th International Conference on the practice and theory of Automated Timetabling

PATAT 2018 - Proceedings of the 12th International Conferenc...

引用

12th International Conference on the practice and theory of Automated Timetabling, PATAT 2018

ISBN: (纸本)9780992998424

The proceedings contain 40 papers. The topics discussed include: an integer programming approach for the physician rostering problem;constraint reformulation for nurse rostering problems;a unified nurse rostering model based on XHSTT;modeling history in nurse rostering;KHE18: a solver for nurse rostering;bi-criteria simulated annealing algorithms for the robust university course timetabling problem;scheduling matters some potential requirements for future rostering competitions from a practitioner's view;and optimizing mobility services.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Constraint Answer Set programming without Grounding

Constraint Answer Set Programming without Grounding

引用

34th International Conference on logic programming (ICLP)

作者： Arias, Joaquin Carro, Manuel Salazar, Elmer Marple, Kyle Gupta, Gopal IMDEA Software Inst Madrid Spain Univ Politecn Madrid Madrid Spain Univ Texas Dallas Richardson TX 75083 USA

Extending ASP with constraints (CASP) enhances its expressiveness and performance. This extension is not straightforward as the grounding phase, present in most ASP systems, removes variables and the links among them, and also causes a combinatorial explosion in the size of the program. Several methods to overcome this issue have been devised: restricting the constraint domains (e.g., discrete instead of dense), or the type (or number) of models that can be returned. In this paper we propose to incorporate constraints into s(ASP), a goal-directed, top-down execution model which implements ASP while retaining logical variables both during execution and in the answer sets. The resulting model, s(CASP), can constrain variables that, as in CLP, are kept during the execution and in the answer sets. s(CASP) inherits and generalizes the execution model of s(ASP) and is parametric w.r.t. the constraint solver. We describe this novel execution model and show through several examples the enhanced expressiveness of s(CASP) w.r.t. ASP, CLP, and other CASP systems. We also report improved performance w.r.t. other very mature, highly optimized ASP systems in some benchmarks.

关键词： Benchmarking

来源：评论

学校读者我要写书评

暂无评论

Constraint programming modeling for the task scheduling problem with data storage at MPSoCs 12

Constraint programming modeling for the task scheduling prob...

引用

12th International Conference on the practice and theory of Automated Timetabling, PATAT 2018

作者： Valouxis, Christos Gogos, Christos Alefragis, Panayiotis Theodoridis, George Voros, Nikolaos University of Patras Greece Technological Educational Institute of Epirus Greece Technological Educational Institute of Western Greece Greece

ISBN: (纸本)9780992998424

Multi Processor System on Chips are expected to exhibit increased performance when extra memory chips exist close to their processing units. Given an architecture of such a system, equipped with private fast memories for each processor and a slower shared memory for all of them, we propose a constraint programming model that is capable of scheduling program workflows annotated with data usage information. Our approach examines usage of the data objects by individual tasks and arranges their positioning to certain private memories or to the shared memory during the execution. The objective is to minimize the makespan of the workflow. Experiments on artificially generated workflows show that values close to theoretical lower bounds can be achieved for moderate problem sizes under reasonable execution time. © PATAT 2018 Organizing Committee.

关键词： Multitasking

来源：评论

学校读者我要写书评

暂无评论

Computer-aided proofs for multiparty computation with active security 31

Computer-aided proofs for multiparty computation with active...

引用

31st IEEE Computer Security Foundations Symposium (CSF) held as part of the Federated logic Conference (FLoC)

作者： Haagh, Helene Karbyshev, Aleksandr Oechsner, Sabine Spitters, Bas Strub, Pierre-Yves Aarhus Univ Aarhus Denmark Ecole Polytech Palaiseau France

ISBN: (纸本)9781538666807

Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the output of the function. It has found applications in areas such as auctioning, email filtering, and secure teleconference. Given their importance, it is crucial that the protocols are specified and implemented correctly. In the programming language community, it has become good practice to use computer proof assistants to verify correctness proofs. In the field of cryptography, EasyCrypt is the slate of the art proof assistant. It provides an embedded language for probabilistic programming, together with a specialized logic, embedded into an ambient general purpose higher-order logic. It allows us to conveniently express cryptographic properties. EasyCrypt has been used successfully on many applications, including public-key encryption, signatures, garbled circuits and differential privacy. Here we show for the first time that it can also be used to prove security of MPC against a malicious adversary. We formalize additive and replicated secret sharing schemes and apply them to Maurer's MPC protocol for secure addition and multiplication. Our method extends to general polynomial functions. We follow the insights from EasyCrypt that security proofs can often be reduced to proofs about program equivalence, a topic that is well understood in the verification of programming languages. In particular, we show that for a class of MPC protocols in the passive case the non-interference-based (NI) definition is equivalent to a standard simulation-based security definition. For the active case, we provide a new non-interference based alternative to the usual simulation-based cryptographic definition that is tailored specifically to our protocol.

关键词： Cryptography Protocols Additives Probabilistic logic Standards Tools"

来源：评论

学校读者我要写书评

暂无评论

Majority logic Synthesis 18

Majority Logic Synthesis

引用

37th IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

作者： Amaru, Luca Testa, Eleonora Couceiro, Miguel Zografos, Odysseas De Micheli, Giovanni Soeken, Mathias Synopsys Inc Mountain View CA 94043 USA Ecole Polytech Fed Lausanne Lausanne Switzerland Univ Lorraine Metz France Imec Leuven Belgium

ISBN: (纸本)9781450359504

The majority function (xyz) evaluates to true, if at least two of its Boolean inputs evaluate to true. The majority function has frequently been studied as a central primitive in logic synthesis applications for many decades. Knuth refers to the majority function in the last volume of his seminal The Art of Computer programming as "probably the most important ternary operation in the entire universe." Majority logic sythesis has recently regained signficant interest in the design automation community due to nanoemerging technologies which operate based on the majority function. In addition, majority logic synthesis has successfully been employed in CMOS-based applications such as standard cell or FPGA mapping. This tutorial gives a broad introduction into the field of majority logic synthesis. It will review fundamental results and and describe recent contributions from theory, practice, and applications.

关键词： Boolean functions Optimization Tutorials logic gates Binary decision diagrams Inverters

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：