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

Quantifiers on demand

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Gurfinkel, Arie Buchbinder, Sharon Shoham Vizel, Yakir University of Waterloo Tel Aviv University The Technion

Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference and reasoning with universally quantified formulas. In this paper, we present a new algorithm, QUIC3, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, QUIC3 carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While QUIC3 is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions. We have implemented QUIC3 within the Constrained Horn Clause solver engine of Z3 and experimented with it by applying QUIC3 to verifying a variety of public benchmarks of array manipulating C programs. Copyright © 2021, The Authors. All rights reserved.

关键词： logic programming

Graph-based interpretation of normal logic programs

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Li, Fang Salazar, Elmer Gupta, Gopal The University of Texas at Dallas RichardsonTX75080 United States

In this paper we present a dependency graph-based method for computing the various semantics of normal logic programs. Our method employs conjunction nodes to unambiguously represent the dependency graph of normal logic programs. The dependency graph can be transformed suitably in a semantics preserving manner and re-translated into a equivalent normal logic program. This transformed normal logic program can be augmented with a few rules written in answer set programming (ASP), and the CLINGO system used to compute its answer sets. Depending on how these additional rules are coded in ASP, one can compute models of the original normal logic program under the stable model semantics, the well-founded semantics, or the co-stable model semantics. In each case, justification for each atom in the model is also generated. We report on the implementation of our method as well as its performance evaluation. © 2021, CC BY.

关键词： logic programming

ON SYNTACTICALLY SIMILAR logic PROGRAMS AND SEQUENTIAL DECOMPOSITIONS

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Antić, Christian Vienna Austria

Rule-based reasoning is an essential part of human intelligence prominently formalized in artificial intelligence research via logic programs. Describing complex objects as the composition of elementary ones is a common strategy in computer science and science in general. The author has recently introduced the sequential composition of logic programs in the context of logic-based analogical reasoning and learning in logic programming. Motivated by these applications, in this paper we construct a qualitative and algebraic notion of syntactic logic program similarity from sequential decompositions of programs. We then show how similarity can be used to answer queries across different domains via a one-step reduction. In a broader sense, this paper is a further step towards an algebraic theory of logic programming. Copyright © 2021, The Authors. All rights reserved.

关键词： logic programming

Extending Data Spatial Semantics for Scale Agnostic programming

学校读者我要写书评

暂无评论

arXiv 2025年

作者： Mars, Jason University of Michigan 2260 Hayward St. Ann ArborMI48104 United States

We introduce extensions to Data Spatial programming (DSP) that enable scale-agnostic programming for application development. Building on DSP’s paradigm shift from "data-to-compute" to "compute-to-data," we formalize additional intrinsic language constructs that abstract persistent state, multi-user contexts, multiple entry points, and cross-machine distribution for applications. By introducing a globally accessible root node and treating walkers as potential entry points, we demonstrate how programs can be written once and executed across scales—from single-user to multi-user, from local to distributed—without modification. These extensions allow developers to focus on domain logic while delegating runtime concerns of persistence, multi-user support, distribution, and API interfacing to the execution environment. Our approach makes scale-agnostic programming a natural extension of the topological semantics of DSP, allowing applications to seamlessly transition from single-user to multi-user scenarios, from ephemeral to persistent execution contexts, and from local to distributed execution environments. © 2025, CC BY-NC-ND.

关键词： logic programming

Solving a Multi-resource partial-ordering flexible variant of the job-shop scheduling problem with hybrid ASP

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Francescutto, Giulia Schekotihin, Konstantin El-Kholany, Mohammed M.S. Infineon Technologies Austria AG Siemensstrasse 2 Villach9500 Austria University of Klagenfurt Universitaetsstrasse 65-67 Klagenfurt Austria

Many complex activities of production cycles, such as quality control or fault analysis, require highly experienced specialists to perform various operations on (semi)finished products using different tools. In practical scenarios, the selection of a next operation is complicated, since each expert has only a local view on the total set of operations to be performed. As a result, decisions made by the specialists are suboptimal and might cause significant costs. In this paper, we consider a Multi-resource Partial-ordering Flexible Job-shop Scheduling (MPF-JSS) problem where partially-ordered sequences of operations must be scheduled on multiple required resources, such as tools and specialists. The resources are flexible and can perform one or more operations depending on their properties. The problem is modeled using Answer Set programming (ASP) in which the time assignments are efficiently done using Difference logic. Moreover, we suggest two multi-shot solving strategies aiming at the identification of the time bounds allowing for a solution of the schedule optimization problem. Experiments conducted on a set of instances extracted from a medium-sized semiconductor fault analysis lab indicate that our approach can find schedules for 87 out of 91 considered real-world instances. © 2021, CC BY.

关键词： logic programming

Generating explanations for answer set programming applications

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Trieu, Ly Ly Son, Tran Cao Pontelli, Enrico Balduccini, Marcello New Mexico State University MSC CS PO Box 30001 Las CrucesNM United States Saint Joseph’s University 5600 City Avenue PhiladelphiaPA United States

We present an explanation system for applications that leverage Answer Set programming (ASP). Given a program P, an answer set A of P, and an atom a in the program P, our system generates all explanation graphs of a which help explain why a is true (or false) given the program P and the answer set A. We illustrate the functionality of the system using some examples from the literature. © 2021, CC BY.

关键词： logic programming

Learning first-order representations for planning from black-box states: New results

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Rodriguez, Ivan D. Bonet, Blai Romero, Javier Geffner, Hector Universitat Pompeu Fabra Spain University of Potsdam Germany ICREA and Universitat Pompeu Fabra Spain

Recently Bonet and Geffner have shown that first-order representations for planning domains can be learned from the structure of the state space without any prior knowledge about the action schemas or domain predicates. For this, the learning problem is formulated as the search for a simplest first-order domain description D that along with information about instances Ii(number of objects and initial state) determine state space graphs G(Pi) that match the observed state graphs Giwhere Pi= 〈D, Ii〉. The search is cast and solved approximately by means of a SAT solver that is called over a large family of propositional theories that differ just in the parameters encoding the possible number of action schemas and domain predicates, their arities, and the number of objects. In this work, we push the limits of these learners by moving to an answer set programming (ASP) encoding using the CLINGO system. The new encodings are more transparent and concise, extending the range of possible models while facilitating their exploration. We show that the domains introduced by Bonet and Geffner can be solved more efficiently in the new approach, often optimally, and furthermore, that the approach can be easily extended to handle partial information about the state graphs as well as noise that prevents some states from being distinguished. Copyright © 2021, The Authors. All rights reserved.

关键词： logic programming

Operating room (Re)scheduling with bed management via ASP

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Dodaro, Carmine Galatà, Giuseppe Khan, Muhammad Kamran Maratea, Marco Porro, Ivan University of Calabria Italy SurgiQ srl Italy University of Genoa Italy

The Operating Room Scheduling (ORS) problem is the task of assigning patients to operating rooms, taking into account different specialties, lengths and priority scores of each planned surgery, operating room session durations, and the availability of beds for the entire length of stay both in the Intensive Care Unit and in the wards. A proper solution to the ORS problem is of primary importance for the healthcare service quality and the satisfaction of patients in hospital environments. In this paper we first present a solution to the problem based on Answer Set programming (ASP). The solution is tested on benchmarks with realistic sizes and parameters, on three scenarios for the target length on 5-day scheduling, common in small-medium sized hospitals, and results show that ASP is a suitable solving methodology for the ORS problem in such setting. Then, we also performed a scalability analysis on the schedule length up to 15 days, which still shows the suitability of our solution also on longer plan horizons. Moreover, we also present an ASP solution for the rescheduling problem, i.e. when the off-line schedule cannot be completed for some reason. Finally, we introduce a web framework for managing ORS problems via ASP that allows a user to insert the main parameters of the problem, solve a specific instance, and show results graphically in real-time. Under consideration in Theory and Practice of logic programming (TPLP).12. Copyright © 2021, The Authors. All rights reserved.

关键词： logic programming

FOLASP: FO(·) as input language for answer set solvers

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Dessel, Kylian Van Devriendt, Jo Vennekens, Joost KU Leuven Dept. of Computer Science De Nayer Campus Sint-Katelijne-Waver Belgium Leuven.AI – KU Leuven Institute for AI Leuven Belgium

Over the past decades, Answer Set programming (ASP) has emerged as an important paradigm for declarative problem solving. Technological progress in this area has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in non-monotonic reasoning, efforts have also been made to reconcile ASP with classical first-order logic (FO). 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(·). © 2021, CC BY.

关键词： logic programming