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

26th International Conference on Principles and practice of Declarative programming (PPDP)

作者： Arias, Jaime Olarte, Carlos Petrucci, Laure Penczek, Wojciech Sidoruk, Teofil Univ Sorbonne Paris Nord LIPN CNRS UMR 7030 Villetaneuse France Polish Acad Sci Inst Comp Sci Warsaw Poland

ISBN: (纸本)9798400709692

Strategic Timed CTL (STCTL) is an expressive logic that integrates branching time CTL with the representation of continuous time, and the notion of strategic abilities of agents. This makes STCTL suitable for specifying properties of asynchronous multi-agent systems modeled as networks of Parametric Timed Automata (PTA). Existing model checkers and synthesis procedures for STCTL are often limited in scope (bounded analyses), rely on ad-hoc implementations, and are difficult to prove correct. In this paper we propose declarative methods for STCTL model checking and synthesis using rewriting logic. Our approach uses rewriting modulo SMT to represent clock constraints and timed parameters as terms in a rewrite theory, and we adequately capture the continuous semantics of STCTL via rewriting strategies. The resulting algebraic specification is executable in the rewrite engine Maude. This is a novel application of Maude's strategy language and, since our procedures are grounded on logical means, it is simpler to prove them correct. Our approach advances the state of the art for the analysis of multi-agent systems by allowing for the nesting of temporal operators and universal STCTL formulas, which have not been considered before. We benchmark our rewrite theory against existing procedures for STCTL, demonstrating competitive performance and even outperforming dedicated procedures for the existential fragment of STCTL. We thus provide a more robust and verifiable approach to STCTL model checking and synthesis.

关键词： Rewriting logic Maude Model Checking Timed Automata

来源：评论

学校读者我要写书评

暂无评论

Specifying and Reasoning about CPS through the Lens of the NIST CPS Framework

引用

theory and practice of logic programming 2023年第5期23卷 1029-1069页

作者： Thanh Hai Nguyen Bundas, Matthew Son, Tran Cao Balduccini, Marcello Garwood, Kathleen Campbell Griffor, Edward R. New Mexico State Univ Dept Comp Sci Las Cruces NM 88003 USA St Josephs Univ Philadelphia PA 19131 USA NIST Gaithersburg MD 20899 USA

This paper introduces a formal definition of a Cyber-Physical System (CPS) in the spirit of the CPS Framework proposed by the National Institute of Standards and Technology (NIST). It shows that using this definition, various problems related to concerns in a CPS can be precisely formalized and implemented using Answer Set programming (ASP). These include problems related to the dependency or conflicts between concerns, how to mitigate an issue, and what the most suitable mitigation strategy for a given issue would be. It then shows how ASP can be used to develop an implementation that addresses the aforementioned problems. The paper concludes with a discussion of the potentials of the proposed methodologies.

关键词： artificial intelligence knowledge representation automated reasoning and planning cyber-physical system answer set programming concern satisfaction CPS ontology

来源：评论

学校读者我要写书评

暂无评论

Neuro-Symbolic AI for Compliance Checking of Electrical Control Panels

引用

theory and practice of logic programming 2023年第4期23卷 748-764页

作者： Barbara, Vito Leone, Nicola Ricca, Francesco Guarascio, Massimo Manco, Giuseppe Quarta, Alessandro Ritacco, Ettore Univ Calabria Arcavacata Di Rende Italy ICAR CNR Arcavacata Di Rende Italy Sapienza Univ Rome Rome Italy Univ Udine Udine Italy

Artificial Intelligence plays a main role in supporting and improving smart manufacturing and Industry 4.0, by enabling the automation of different types of tasks manually performed by domain experts. In particular, assessing the compliance of a product with the relative schematic is a time-consuming and prone-to-error process. In this paper, we address this problem in a specific industrial scenario. In particular, we define a Neuro-Symbolic approach for automating the compliance verification of the electrical control panels. Our approach is based on the combination of Deep Learning techniques with Answer Set programming (ASP), and allows for identifying possible anomalies and errors in the final product even when a very limited amount of training data is available. The experiments conducted on a real test case provided by an Italian Company operating in electrical control panel production demonstrate the effectiveness of the proposed approach.

关键词： automated quality control systems answer set programming computer vision data scarcity

来源：评论

学校读者我要写书评

暂无评论

Parallel logic programming: A Sequel

引用

theory and practice of logic programming 2022年第6期22卷 905-973页

作者： Dovier, Agostino Formisano, Andrea Gupta, Gopal Hermenegildo, Manuel, V Pontelli, Enrico Rocha, Ricardo Univ Udine Udine Italy GNCS INdAM Udine Italy Univ Texas Dallas Austin TX 78712 USA Univ Politecn Madrid IMDEA Software Inst Madrid Spain New Mexico State Univ Las Cruces NM 88003 USA Univ Porto CRACS INESC TEC Porto Portugal Univ Porto Fac Sci Porto Portugal

Multi-core and highly connected architectures have become ubiquitous, and this has brought renewed interest in language-based approaches to the exploitation of parallelism. Since its inception, logic programming has been recognized as a programming paradigm with great potential for automated exploitation of parallelism. The comprehensive survey of the first twenty years of research in parallel logic programming, published in 2001, has served since as a fundamental reference to researchers and developers. The contents are quite valid today, but at the same time the field has continued evolving at a fast pace in the years that have followed. Many of these achievements and ongoing research have been driven by the rapid pace of technological innovation, that has led to advances such as very large clusters, the wide diffusion of multi-core processors, the game-changing role of general-purpose graphic processing units, and the ubiquitous adoption of cloud computing. This has been paralleled by significant advances within logic programming, such as tabling, more powerful static analysis and verification, the rapid growth of Answer Set programming, and in general, more mature implementations and systems. This survey provides a review of the research in parallel logic programming covering the period since 2001, thus providing a natural continuation of the previous survey. In order to keep the survey self-contained, it restricts its attention to parallelization of the major logic programming languages (Prolog, Datalog, Answer Set programming) and with an emphasis on automated parallelization and preservation of the sequential observable semantics of such languages. The goal of the survey is to serve not only as a reference for researchers and developers of logic programming systems but also as engaging reading for anyone interested in logic and as a useful source for researchers in parallel systems outside logic programming.

关键词： parallelism high-performance computing logic programming

来源：评论

学校读者我要写书评

暂无评论

Symbolic Specialization of Rewriting logic Theories with Presto

引用

theory and practice of logic programming 2022年第3期22卷 444-495页

作者： Alpuente, Maria Escobar, Santiago Sapina, Julia Ballis, Demis Univ Politecn Valencia VRAIN Valencian Res Inst Artificial Intelligence Valencia Spain Univ Udine DMIF Udine Italy

This paper introduces Presto, a symbolic partial evaluator for Maude's rewriting logic theories that can improve system analysis and verification. In Presto, the automated optimization of a conditional rewrite theory R (whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of R, an underlying, companion equational logic theory E that specifies the algebraic structure of the system states of R. This can be particularly useful for specializing an overly general equational theory E whose operators may obey complex combinations of associativity, commutativity, and/or identity axioms, when being plugged into a host rewrite theory R as happens, for instance, in protocol analysis, where sophisticated equational theories for cryptography are used. Presto implements different unfolding operators that are based on folding variant narrowing (the symbolic engine of Maude's equational theories). When combined with an appropriate abstraction algorithm, they allow the specialization to be adapted to the theory termination behavior and bring significant improvement while ensuring strong correctness and termination of the specialization. We demonstrate the effectiveness of Presto in several examples of protocol analysis where it achieves a significant speed-up. Actually, the transformation provided by Presto may cut down an infinite folding variant narrowing space to a finite one, and moreover, some of the costly algebraic axioms and rule conditions may be eliminated as well. As far as we know, this is the first partial evaluator for Maude that respects the semantics of functional, logic, concurrent, and object-oriented computations.

关键词： multi-paradigm declarative programming partial evaluation rewriting logic narrowing

来源：评论

学校读者我要写书评

暂无评论

On Correctness and Completeness of an n Queens Program

引用

theory and practice of logic programming 2022年第1期22卷 37-50页

作者： Drabent, Wlodzimierz Polish Acad Sci Inst Comp Sci Ul Jana Kazimierza 5 PL-01248 Warsaw Poland Linkoping Univ Dept Comp & Informat Sci S-58183 Linkoping Sweden

Thom Fruhwirth presented a short, elegant, and efficient Prolog program for the n queens problem. However, the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a declarative way and provides proofs of its correctness and completeness. The specification and the proofs are declarative, that is they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program's semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, based on logical consequence and Herbrand interpretations. Another purpose of the paper is to present an example of precise declarative reasoning about the semantics of a logic program.

关键词： logic programming declarative programming program completeness program correctness specification nonground answers

来源：评论

学校读者我要写书评

暂无评论

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

34th European Symposium on Programming, ESOP 2025, which was...

引用

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

ISBN: (纸本)9783031911170

The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Programs;Constructive characterisations of the MUST-preorder for asynchrony;abstraction of memory block manipulations by symbolic loop folding;cognacy Queries over Dependence Graphs for Transparent Visualisations;an abstract, certified account of operational game semantics;artifact Report: an Abstract, Certified Account of Operational Game Semantics;neural Network Verification is a programming Language Challenge;stratified Type theory;coverage Semantics for Dependent Pattern Matching;variable Elimination as Rewriting in a Linear Lambda Calculus;a Program logic for Concurrent Randomized Programs in the Oblivious Adversary Model;iso-Recursive Multiparty Sessions and their Automated Verification;verifying Algorithmic Versions of the Lovász Local Lemma;Elucidating Type Conversions in SQL Engines.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Efficient Lifting of Symmetry Breaking Constraints for Complex Combinatorial Problems

引用

theory and practice of logic programming 2022年第4期22卷 606-622页

作者： Tarzariol, Alice Schekotihin, Konstantin Gebser, Martin Law, Mark Univ Klagenfurt Klagenfurt Austria Graz Univ Technol Graz Austria Imperial Coll London London England

Many industrial applications require finding solutions to challenging combinatorial problems. Efficient elimination of symmetric solution candidates is one of the key enablers for high-performance solving. However, existing model-based approaches for symmetry breaking are limited to problems for which a set of representative and easily solvable instances is available, which is often not the case in practical applications. This work extends the learning framework and implementation of a model-based approach for Answer Set programming to overcome these limitations and address challenging problems, such as the Partner Units Problem. In particular, we incorporate a new conflict analysis algorithm in the Inductive logic programming system ILASP, redefine the learning task, and suggest a new example generation method to scale up the approach. The experiments conducted for different kinds of Partner Units Problem instances demonstrate the applicability of our approach and the computational benefits due to the first-order constraints learned.

关键词： answer set programming inductive logic programming symmetry breaking constraints

来源：评论

学校读者我要写书评

暂无评论

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

34th European Symposium on Programming, ESOP 2025, which was...

引用

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

ISBN: (纸本)9783031911200

关键词：

来源：评论

学校读者我要写书评

暂无评论

The Semantics of Metaprogramming in Prolog

引用

theory and practice of logic programming 2024年第4期24卷 885-900页

作者： Warren, David scott SUNY Stony Brook Stony Brook NY 11794 USA XSB Inc Setauket NY USA

This paper describes a semantics for pure Prolog programs with negation that provides meaning to metaprograms. Metaprograms are programs that construct and use data structures as programs. In Prolog a primary mataprogramming construct is the use of a variable as a literal in the body of a clause. The traditional Prolog 3-line metainterpreter is another example of a metaprogram. The account given here also supplies a meaning for clauses that have a variable as head, even though most Prolog systems do not support such clauses. This semantics naturally includes such programs, giving them their intuitive meaning. Ideas from Denecker and his colleagues form the basis of this approach. The key idea is to notice that if we give meanings to all propositional programs and treat Prolog rules with variables as the set of their ground instances, then we can give meanings to all programs. We must treat Prolog rules (which may be metarules) as templates for generating ground propositional rules, and not as first-order formulas, which they may not be. We use parameterized inductive definitions to give propositional models to Prolog programs, in which the propositions are expressions. Then the set of expressions of a propositional model determine a first-order Herbrand Model, providing a first-order logical semantics for all (pure) Prolog programs, including metaprograms. We give examples to show the applicability of this theory. We also demonstrate how this theory makes proofs of some important properties of metaprograms very straightforward.

关键词： inductive definitions prolog semantics programming language semantics interpretation

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：