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

Extensible Metatheory Mechanization via Family Polymorphism

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2023年第PLDI期7卷 1608-1632页

作者： Jin, Ende Amin, Nada Zhang, Yizhou Univ Waterloo Cheriton Sch Comp Sci Waterloo ON Canada Harvard Univ Paulson Sch Engn & Appl Sci Cambridge MA USA

With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs. This paper presents a novel language design geared towards extensible metatheory mechanization in a proof assistant. The new design achieves reuse and extensibility via a form of family polymorphism, an object-oriented idea, that allows code and proofs to be polymorphic to their enclosing families. Our development addresses technical challenges that arise from the underlying language of a proof assistant being simultaneously functional, dependently typed, a logic, and an interactive tool. Our results include (1) a prototypical implementation of the language design as a Coq plugin, (2) a dependent type theory capturing the essence of the language mechanism and its consistency and canonicity results, and (3) case studies showing how the new expressiveness naturally addresses real programming challenges in metatheory mechanization.

关键词： Proof engineering interactive theorem proving expression problem inductive types extensible frameworks modules mixins reuse late binding dependent type theory Coq

来源：评论

学校读者我要写书评

暂无评论

Thirty years of Epistemic Specifications

引用

theory and practice of logic programming 2022年第6期22卷 1043-1083页

作者： Fandinno, Jorge Faber, Wolfgang Gelfond, Michael Univ Nebraska Omaha Omaha NE 68182 USA Univ Potsdam Potsdam Germany Alpen Adria Univ Klagenfurt Klagenfurt Austria Texas Tech Univ Lubbock TX 79409 USA

The language of epistemic specifications and epistemic logic programs extends disjunctive logic programs under the stable model semantics with modal constructs called subjective literals. Using subjective literals, it is possible to check whether a regular literal is true in every or some stable models of the program, those models, in this context also called belief sets, being collected in a set called world view. This allows for representing, within the language, whether some proposition should be understood accordingly to the open or the closed world assumption. Several attempts for capturing the intuitions underlying the language by means of a formal semantics were given, resulting in a multitude of proposals that makes it difficult to understand the current state of the art. In this article, we provide an overview of the inception of the field and the knowledge representation and reasoning tasks it is suitable for. We also provide a detailed analysis of properties of proposed semantics, and an outlook of challenges to be tackled by future research in the area.

关键词： answer set programming epistemic logic programs epistemic specifications epistemic reasoning autopistemic logic

来源：评论

学校读者我要写书评

暂无评论

FOLD-RM: A Scalable, Efficient, and Explainable Inductive Learning Algorithm for Multi-Category Classification of Mixed Data

引用

theory and practice of logic programming 2022年第5期22卷 658-677页

作者： Wang, Huaduo Shakerin, Farhad Gupta, Gopal Univ Texas Dallas Richardson TX 75083 USA

FOLD-RM is an automated inductive learning algorithm for learning default rules for mixed (numerical and categorical) data. It generates an (explainable) answer set programming (ASP) rule set for multi-category classification tasks while maintaining efficiency and scalability. The FOLD-RM algorithm is competitive in performance with the widely used, state-of-the-art algorithms such as XGBoost and multi-layer perceptrons, however, unlike these algorithms, the FOLD-RM algorithm produces an explainable model. FOLD-RM outperforms XGBoost on some datasets, particularly large ones. FOLD-RM also provides human-friendly explanations for predictions.

关键词： explainable AI data mining inductive logic programming machine learning

来源：评论

学校读者我要写书评

暂无评论

Knowledge-based Reasoning and Learning under Partial Observability in Ad Hoc Teamwork

引用

theory and practice of logic programming 2023年第4期23卷 696-714页

作者： Dodampegama, Hasra Sridharan, Mohan Univ Birmingham Sch Comp Sci Intelligent Robot Lab Birmingham England

Ad hoc teamwork (AHT) refers to the problem of enabling an agent to collaborate with teammates without prior coordination. State of the art methods in AHT are data-driven, using a large labeled dataset of prior observations to model the behavior of other agent types and to determine the ad hoc agent's behavior. These methods are computationally expensive, lack transparency, and make it difficult to adapt to previously unseen changes. Our recent work introduced an architecture that determined an ad hoc agent's behavior based on non-monotonic logical reasoning with prior commonsense domain knowledge and models learned from limited examples to predict the behavior of other agents. This paper describes KAT, a knowledge-driven architecture for AHT that substantially expands our prior architecture's capabilities to support: (a) online selection, adaptation, and learning of the behavior prediction models;and (b) collaboration with teammates in the presence of partial observability and limited communication. We illustrate and experimentally evaluate KAT's capabilities in two simulated benchmark domains for multiagent collaboration: Fort Attack and Half Field Offense. We show that KAT's performance is better than a purely knowledge-driven baseline, and comparable with or better than a state of the art data-driven baseline, particularly in the presence of limited training data, partial observability, and changes in team composition.

关键词： knowledge representation non-monotonic logical reasoning ecological rationality ad hoc teamwork applications of logic programming

来源：评论

学校读者我要写书评

暂无评论

Efficient Knowledge Compilation Beyond Weighted Model Counting

引用

theory and practice of logic programming 2022年第4期22卷 505-522页

作者： KIESEL, R. A. F. A. E. L. TOTIS, P. I. E. T. R. O. KIMMIG, A. N. G. E. L. I. K. A. TU Wien Vienna Austria Katholieke Univ Leuven Leuven Belgium

Quantitative extensions of logic programming often require the solution of so called second level inference tasks, that is, problems that involve a third operation, such as maximization or normalization, on top of addition and multiplication, and thus go beyond the well-known weighted or algebraic model counting setting of probabilistic logic programming under the distribution semantics. We introduce Second Level Algebraic Model Counting (2AMC) as a generic framework for these kinds of problems. As 2AMC is to (algebraic) model counting what forall-exists-SAT is to propositional satisfiability, it is notoriously hard to solve. First level techniques based on Knowledge Compilation (KC) have been adapted for specific 2AMC instances by imposing variable order constraints on the resulting circuit. However, those constraints can severely increase the circuit size and thus decrease the efficiency of such approaches. We show that we can exploit the logical structure of a 2AMC problem to omit parts of these constraints, thus limiting the negative effect. Furthermore, we introduce and implement a strategy to generate a sufficient set of constraints statically, with a priori guarantees for the performance of KC. Our empirical evaluation on several benchmarks and tasks confirms that our theoretical results can translate into more efficient solving in practice.

关键词： design analysis and implementation of languages logic programming methodology and applications

来源：评论

学校读者我要写书评

暂无评论

Abstract Environment Trimming

引用

theory and practice of logic programming 2024年第4期24卷 863-884页

作者： Jurjo-rivas, Daniel Morales, Jose F. Lopez-garcia, Pedro Hermenegildo, Manuel, V Univ Politecn Madrid UPM IMDEA Software Inst Madrid Spain IMDEA Software Inst Spanish Council Sci Res Madrid Spain

Variable sharing is a fundamental property in the static analysis of logic programs, since it is instrumental for ensuring correctness and increasing precision while inferring many useful program properties. Such properties include modes, determinacy, non-failure, cost, etc. This has motivated significant work on developing abstract domains to improve the precision and performance of sharing analyses. Much of this work has centered around the family of set-sharing domains, because of the high precision they offer. However, this comes at a price: their scalability to a wide set of realistic programs remains challenging and this hinders their wider adoption. In this work, rather than defining new sharing abstract domains, we focus instead on developing techniques which can be incorporated in the analyzers to address aspects that are known to affect the efficiency of these domains, such as the number of variables, without affecting precision. These techniques are inspired in others used in the context of compiler optimizations, such as expression reassociation and variable trimming. We present several such techniques and provide an extensive experimental evaluation of over 1100 program modules taken from both production code and classical benchmarks. This includes the Spectector cache analyzer, the s(CASP) system, the libraries of the Ciao system, the LPdoc documenter, the PLAI analyzer itself, etc. The experimental results are quite encouraging: we have obtained significant speedups, and, more importantly, the number of modules that require a timeout was cut in half. As a result, many more programs can be analyzed precisely in reasonable times.

关键词： logic programming methodology and applications specification analysis and verification of systems security

来源：评论

学校读者我要写书评

暂无评论

ValAsp: A Tool for Data Validation in Answer Set programming

引用

theory and practice of logic programming 2023年第5期23卷 965-985页

作者： Alviano, Mario Dodaro, Carmine Zamayla, Arnel Univ Calabria Dept Math & Comp Sci Via P BucciCubo 30B I-87036 Arcavacata Di Rende CS Italy

The development of complex software requires tools promoting fail-fast approaches, so that bugs and unexpected behavior can be quickly identified and fixed. Tools for data validation may save the day of computer programmers. In fact, processing invalid data is a waste of resources at best, and a drama at worst if the problem remains unnoticed and wrong results are used for business. Answer Set programming (ASP) is not an exception, but the quest for better and better performance resulted in systems that essentially do not validate data. Even under the simplistic assumption that input/output data are eventually validated by external tools, invalid data may appear in other portions of the program, and go undetected until some other module of the designed software suddenly breaks. This paper formalizes the problem of data validation for ASP programs, introduces a language to specify data validation, and presents valasp, a tool to inject data validation in ordinary programs. The proposed approach promotes fail-fast techniques at coding time without imposing any lag on the deployed system if data are pretended to be valid. Validation can be specified in terms of statements using YAML, ASP and Python. Additionally, the proposed approach opens the possibility to use ASP for validating data of imperative programming languages.

关键词： Answer Set programming data validation secure coding fail-fast

来源：评论

学校读者我要写书评

暂无评论

Analysis and Transformation of Constrained Horn Clauses for Program Verification

引用

theory and practice of logic programming 2022年第6期22卷 974-1042页

作者： De Angelis, Emanuele Fioravanti, Fabio Gallagher, John P. Hermenegildo, Manuel, V Pettorossi, Alberto Proietti, Maurizio IASI CNR Rome Italy Univ G DAnnunzio DEC Chieti Italy Roskilde Univ Roskilde Denmark IMDEA Software Inst Madrid Spain Univ Politecn Madrid UPM Madrid Spain Univ RomeTor Vergata DICII Rome Italy

This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialization-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialization and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.

关键词： Program verification program analysis program transformation constrained Horn clauses constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Early Validation of High-Level System Requirements with Event Calculus and Answer Set programming

引用

theory and practice of logic programming 2024年第4期24卷 844-862页

作者： Vasicek, Ondrej Arias, Joaquin Fiedor, Jan Gupta, Gopal Hall, Brendal Krena, Bohuslav Larson, Brian Varanasi, Sarat chandra Vojnar, Tomas Brno Univ Technol Fac Informat Technol Brno Czech Republic Univ Rey Juan Carlos Mostoles Spain Honeywell Int SRO Brno Czech Republic UT Dallas Comp Sci Dept Richardson TX USA Ardent Innovat Labs Eden Prairie MN USA Multitude Corp St Paul MN USA GE Aerosp Res Niskayuna NY USA Masaryk Univ Fac Informat Brno Czech Republic

This paper proposes a new methodology for early validation of high-level requirements on cyber-physical systems with the aim of improving their quality and, thus, lowering chances of specification errors propagating into later stages of development where it is much more expensive to fix them. The paper presents a transformation of a real-world requirements specification of a medical device-the Patient-Controlled Analgesia (PCA) Pump-into an Event Calculus model that is then evaluated using Answer Set programming and the s(CASP) system. The evaluation under s(CASP) allowed deductive as well as abductive reasoning about the specified functionality of the PCA pump on the conceptual level with minimal implementation or design dependent influences and led to fully automatically detected nuanced violations of critical safety properties. Further, the paper discusses scalability and non-termination challenges that had to be faced in the evaluation and techniques proposed to (partially) solve them. Finally, ideas for improving s(CASP) to overcome its evaluation limitations that still persist as well as to increase its expressiveness are presented.

关键词： requirements validation event calculus answer set programming s(CASP)

来源：评论

学校读者我要写书评

暂无评论

Automating Semantic Analysis of System Assurance Cases Using Goal-Directed ASP

引用

theory and practice of logic programming 2024年第4期24卷 805-824页

作者： Murugesan, Anitha Wong, Isaac Arias, Joaquin Stroud, Robert Varadarajan, Srivatsan Salazar, Elmer Gupta, Gopal Bloomfield, Robin Rushby, John Honeywell Aerosp Plymouth MN 55441 USA Univ Rey Juan Carlos CETINIA Madrid Spain Adelard Part NCC Grp London England Univ Texas Dallas Dallas TX USA City Univ London London England SRI Int Menlo Pk CA USA

Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools focus on automating structural aspects, they lack the ability to fully assess the semantic coherence and correctness of the assurance *** prior work, we introduced the Assurance 2.0 framework that prioritizes the reasoning process, evidence utilization, and explicit delineation of counter-claims (defeaters) and counter-evidence. In this paper, we present our approach to enhancing Assurance 2.0 with semantic rule-based analysis capabilities using common-sense reasoning and answer set programming solvers, specifically s(CASP). By employing these analysis techniques, we examine the unique semantic aspects of assurance cases, such as logical consistency, adequacy, indefeasibility, etc. The application of these analyses provides both system developers and evaluators with increased confidence about the assurance case.

关键词： automated assurance reasoning semantic analysis answer set programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：