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

Determining Action Reversibility in STRIPS Using answer set and Epistemic Logic programming

THEORY AND PRACTICE OF LOGIC programming 2021年第5期21卷 646-662页

作者： Faber, Wolfgang Morak, Michael Chrpa, Lukas Univ Klagenfurt Klagenfurt Austria Czech Tech Univ Prague Czech Republic

In the context of planning and reasoning about actions and change, we call an action reversible when its effects can be reverted by applying other actions, returning to the original state. Renewed interest in this area has led to several results in the context of the PDDL language, widely used for describing planning tasks. In this paper, we propose several solutions to the computational problem of deciding the reversibility of an action. In particular, we leverage an existing translation from PDDL to answer set programming (ASP), and then use several different encodings to tackle the problem of action reversibility for the STRIPS fragment of PDDL. For these, we use ASP, as well as Epistemic Logic programming (ELP), an extension of ASP with epistemic operators, and compare and contrast their strengths and weaknesses.

关键词： action reversibility answer set programming Epistemic Logic programming reasoning about action and change

来源：评论

学校读者我要写书评

暂无评论

On the Generalization of Learned Constraints for ASP Solving in Temporal Domains

引用

THEORY AND PRACTICE OF LOGIC programming 2025年

作者： Romero, Javier Schaub, Torsten Strauch, Klaus Univ Potsdam Potsdam Brandenburg Germany

The representation of a temporal problem in answer set programming (ASP) usually boils down to using copies of variables and constraints, one for each time stamp, no matter whether it is directly encoded or expressed via an action or temporal language. The multiplication of variables and constraints is commonly done during grounding, and the solver is completely ignorant about the temporal relationship among the different instances. On the other hand, a key factor in the performance of today's ASP solvers is conflict-driven constraint learning. Our question in this paper is whether a constraint learned for particular time steps can be generalized and reused at other time steps, and ultimately whether this enhances the overall solver performance on temporal problems. Knowing well the domain of time, we study conditions under which learned dynamic constraints can be generalized. Notably, we identify a property of temporal representations that enables the generalization of learned constraints across all time steps. It turns out that most ASP planning encodings either satisfy this property or can be easily adapted to do so. In addition, we propose a general translation that transforms programs to fulfill this property. Finally, we empirically evaluate the impact of adding the generalized constraints to an ASP solver.

关键词： answer set programming answer set solving temporal reasoning

来源：评论

学校读者我要写书评

暂无评论

Inductive Synthesis of Inductive Heap Predicates

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2025年第OOPSLA1期9卷 169-195页

作者： Yang, Ziyi Sergey, Ilya Natl Univ Singapore Singapore Singapore

We present an approach to automatically synthesise recursive predicates in Separation Logic (SL) from concrete data structure instances using Inductive Logic programming (ILP) techniques. The main challenges to make such synthesis effective are (1) making it work without negative examples that are required in ILP but are difficult to construct for heap-based structures in an automated fashion, and (2) to be capable of summarising not just the shape of a heap (e.g., it is a linked list), but also the properties of the data it stores (e.g., it is a sorted linked list). We tackle these challenges with a new predicate learning algorithm. The key contributions of our work are (a) the formulation of ILP-based learning only using positive examples and (b) an algorithm that synthesises property-rich SL predicates from concrete memory graphs based on the positive-only learning. We show that our framework can efficiently and correctly synthesise SL predicates for structures that were beyond the reach of the state-of-the-art tools, including those featuring non-trivial payload constraints (e.g., binary search trees) and nested recursion (e.g., n-ary trees). We further extend the usability of our approach by a memory graph generator that produces positive heap examples from programs. Finally, we show how our approach facilitates deductive verification and synthesis of correct-by-construction code.

关键词： inductive program synthesis answer set programming Separation Logic

来源：评论

学校读者我要写书评

暂无评论

Polynomial Formal Verification of Multi-Valued Approximate Circuits Within Constant Cutwidth

引用

IEEE TRANSACTIONS ON CIRCUITS AND SYSTEMS I-REGULAR PAPERS 2025年第3期72卷 1411-1424页

作者： Nadeem, Mohamed Jha, Chandan Kumar Drechsler, Rolf Univ Bremen Dept Math & Comp Sci D-28359 Bremen Germany DFKI GmbH Dept Cyber Phys Syst D-28359 Bremen Germany

Ensuring functional correctness is achieved through formal verification. As circuit complexity increases, limiting the upper bounds for time and space required for verification becomes crucial. Polynomial Formal Verification (PFV) has been introduced to tackle this problem. In modern digital system designs, approximate circuits are widely employed in error resilient applications. Therefore, ensuring the functional correctness of these circuits becomes essential. In prior works, it has been proven that approximate circuits with constant cutwidth can be verified in linear time. However, extending binary logic verification to Multi-Valued Logic (MVL) introduces challenges, particularly regarding the encoding of MVL operators. It has been shown that MVL circuits with constant cutwidth can be verified in linear time using answer set programming (ASP), due to the ASP encoding capabilities of MVL operators. In this paper, we present a PFV approach of MVL approximate circuits with constant cutwidth using ASP. We then demonstrate that the verification of MVL approximate circuits with constant cutwidth can be achieved in linear time. Finally, we evaluate various MVL approximate circuits with constant cutwidth across different logic levels to show the efficacy of our approach.

关键词： Circuits Logic Logic gates Adders Polynomials Formal verification Encoding Inverters Complexity theory Circuit synthesis Polynomial formal verification logic synthesis multi-valued logic approximate circuits answer set programming cutwidth

来源：评论

学校读者我要写书评

暂无评论

Clingo2DSR-A clingo-based software system for declarative spatial reasoning

引用

SPATIAL COGNITION AND COMPUTATION 2025年第1期25卷 69-119页

作者： Li, Beidi Schultz, Carl Aarhus Univ Dept Elect & Comp Engn Aarhus Denmark Aarhus Univ Dept Elect & Comp Engn Helsingforsgade 10 DK-8200 Aarhus Denmark

We present a modified ground-and-solve approach based on the clingo answer set programming (ASP) system to perform non-monotonic spatial reasoning tasks, Clingo2DSR. Our system is distinct from previous research integrating ASP with space in that it deals with complex real-world data and numerous time steps. Clingo2DSR is composed of (i) an input language defining spatial entities, functions, and relations;(ii) an external geometry database for performing spatial computations and checking spatial constraints;and (iii) a theory-based solving approach coupling symbolic ASP with external sources for sound and fast model search. We demonstrate our system on three real building models, in the context of architectural design, submitted for analyses and queries where spatial components play an important role.

关键词： Building Information Modelling answer set programming spatial reasoning

来源：评论

学校读者我要写书评

暂无评论

Integrating Structured Declarative Language (SDL) into ASP Chef 17th

Integrating Structured Declarative Language (SDL) into ASP C...

引用

17th International Conference on Logic programming and Non-monotonic Reasoning

作者： Alviano, Mario Guarasci, Paola Reiners, Luis Angel Rodriguez Vasile, Ilaria R. Univ Calabria DEMACS Via Bucci 30-B I-87036 Arcavacata Di Rende CS Italy

ISBN: (纸本)9783031742088;9783031742095

This article explores the integration of Structured Declarative Language (SDL) into ASP Chef, a low-code web application designed to facilitate the development of pipelines for combinatorial search and optimization. SDL is a recent proposal aimed at simplifying the syntax of answer set programming (ASP), inspired by the straightforwardness of SQL. The integration is achieved through the implementation of a server that compiles SDL specifications into ASP programs and the addition of a new operation in ASP Chef to manage data exchange with the server. This integration aims to streamline the development process and make it more accessible for users working on combinatorial optimization tasks.

关键词： answer set programming declarative languages Combinatorial Search and Optimization system description

来源：评论

学校读者我要写书评

暂无评论

Mutating Clingo's AST with clingabomino 36th

Mutating Clingo's AST with clingabomino

引用

36th International Conference on Testing Software and Systems

作者： Prikler, Liliana Marie Wotawa, Franz Graz Univ Technol Inst Software Technol A-8010 Graz Austria

ISBN: (纸本)9783031808883;9783031808890

Although answer set programming has been a tried way of problem-solving for over thirty years, few tools and methodologies exist today to test it rigorously. Previous research suggests that mutation testing is able to uncover flaws even with small inputs. In this paper, we introduce clingabomino, a mutant generator implemented in C++ that directly operates on the abstract syntax tree of the Clingo solver. Our tool consists of a command-line application that implements commonly useful mutation operators as well as a library to aid in the development of domain-specific mutation operators.

关键词： answer set programming Mutation testing Mutant generation

来源：评论

学校读者我要写书评

暂无评论

Reevaluating the Small-Scope Testing Hypothesis of answer set Programs 36th

Reevaluating the Small-Scope Testing Hypothesis of Answer Se...

引用

36th International Conference on Testing Software and Systems

作者： Prikler, Liliana Marie Wotawa, Franz Graz Univ Technol Inst Software Technol A-8010 Graz Austria

ISBN: (纸本)9783031808883;9783031808890

As we increasingly rely on artificial intelligence systems, we must ensure that those systems are reliable and need to know how much we can rely on them. In software quality assurance, testing is a useful method to highlight and fix issues during development to avoid unexpected behavior after the system has been deployed. Artificial intelligence engineers are increasingly becoming aware of quality assurance as a requirement. Previous results in the area of answer set programming suggest that a high proportion of errors can be found when testing a program against a small scope, i.e. by inputs from a small domain. However, these results are based on assumptions that may be impractical for testing. To find out whether small scopes remain sufficient in practice, we evaluate several benchmarks against actual test oracles. Our findings suggest that small scopes can indeed find a high proportion of errors, but results depend on the observed benchmark and appropriate test oracles are required to achieve reliable scores.

关键词： answer set programming Mutation testing Small-scope hypothesis

来源：评论

学校读者我要写书评

暂无评论

An ILASP-Based Approach to Repair Petri Nets 17th

An ILASP-Based Approach to Repair Petri Nets

引用

17th International Conference on Logic programming and Non-monotonic Reasoning

作者： Chiariello, Francesco Ielo, Antonio Tarzariol, Alice Univ Toulouse IRIT ANITI Toulouse France Univ Calabria Arcavacata Di Rende Italy Univ Klagenfurt Klagenfurt Austria

ISBN: (纸本)9783031742088;9783031742095

Petri nets are a class of models of computation used to compactly represent discrete event systems. Among many application domains, they have now become the most prominent formalism to express process models in Process Mining, thanks to their formal semantics that enables automated analysis techniques. In this context, model repair is the task of aligning a process model with actual executions of the process. Current solutions to model repair do not allow for embedding domain knowledge, providing guarantees of rigor, and enforcing structural requirements at the same time. In this paper, we fill this gap by proposing an approach based on the Inductive Logic programming system ILASP. We then implement our approach and perform an experimental evaluation, showing both its expressiveness and feasibility.

关键词： Petri nets Process Mining Model Repair answer set programming Inductive Logic programming

来源：评论

学校读者我要写书评

暂无评论

An ASP-Based Approach to Water Distribution System Reconstruction 17th

An ASP-Based Approach to Water Distribution System Reconstru...

引用

17th International Conference on Logic programming and Non-monotonic Reasoning

作者： Ielo, Antonio Falco, Salvatore Iiritano, Salvatore Piro, Patrizia Polizzi, Ada Ricca, Francesco Univ Calabria I-87036 Arcavacata Di Rende CS Italy SigmaWater Srl I-87036 Arcavacata Di Rende CS Italy Revelis Srl I-87036 Arcavacata Di Rende CS Italy

ISBN: (纸本)9783031742088;9783031742095

Hydraulic engineering analysis of Water Distribution Systems (WDSs) is performed by running simulation softwares. The starting point to setup a simulation is to reconstruct the WDS topology. In many countries, including Italy, it often happens that data on the WDS is not readily available and accessible in digital format, and topology-reconstruction has to be carried out manually. This paper describes an application of answer set programming to partially automate the task of determining a WDS topology from geospatial data. Also, we report on a real-world use case that shows the feasibility of our approach.

关键词： answer set programming Hydro-informatics Applications

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：