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

An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Alberti, Marco Zese, Riccardo Riguzzi, Fabrizio Lamma, Evelina Dipartimento di Matematica e Informatica University of Ferrara Italy Dipartimento di Scienze Chimiche Farmaceutiche ed Agrarie University of Ferrara Italy Dipartimento di Ingegneria University of Ferrara Italy

Hybrid Knowledge Bases based on Lifschitz’s logic of Minimal Knowledge with Negation as Failure are a successful approach to combine the expressivity of Description logics and logic programming in a single language. Their syntax, defined by Motik and Rosati, disallows function symbols. In order to define a well-founded semantics for MKNF HKBs, Knorr et al. define a partition of the modal atoms occurring in it, called the alternating fixpoint partition. In this paper, we propose an iterated fixpoint semantics for HKBs with function symbols. We prove that our semantics extends Knorr et al.’s, in that, for a function-free HKBs, it coincides with its alternating fixpoint partition. The proposed semantics lends itself well to a probabilistic extension with a distribution semantic approach, which is the subject of future work. © 2022, CC BY.

关键词： logic programming

A note on occur-check (extended report)

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Drabent, Wlodzimierz Institute of Computer Science Polish Academy of Sciences Poland

We weaken the notion of "not subject to occur-check" (NSTO), on which most known results on avoiding the occur-check in logic programming are based. NSTO means that unification is performed only on such pairs of atoms for which the occur-check never succeeds in any run of a nondeterministic unification algorithm. Here we show that "any run" can be weakened to "some run". We present some related sufficient conditions under which the occur-check may be safely omitted. We show examples for which the proposed approach provides more general results than the approaches based on well-moded and nicely moded programs (this includes cases to which the latter approaches are inapplicable). We additionally present a sufficient condition based on NSTO, working for arbitrary selection *** Codes 68N17 03B10 Copyright © 2022, The Authors. All rights reserved.

关键词： logic programming

Using Answer Set programming for HPC Dependency Solving

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Gamblin, Todd Culpo, Massimiliano Becker, Gregory Shudler, Sergei Lawrence Livermore National Laboratory LivermoreCA United States S.r.l np-complete Italy

Modern scientific software stacks have become extremely complex, using many programming models and libraries to exploit a growing variety of GPUs and accelerators. Package managers can mitigate this complexity using dependency solvers, but they are reaching their limits. Finding compatible dependency versions is NP-complete, and modeling the semantics of package compatibility modulo build-time options, GPU runtimes, flags, and other parameters is extremely difficult. Within this enormous configuration space, defining a "good" configuration is daunting. We tackle this problem using Answer Set programming (ASP), a declarative model for combinatorial search problems. We show, using the Spack package manager, that ASP programs can concisely express the compatibility rules of HPC software stacks and provide strong quality-of-solution guarantees. Using ASP, we can mix new builds with preinstalled binaries, and solver performance is acceptable even when considering tens of thousands of packages. © 2022, CC BY.

关键词： logic programming

A Complete Diagrammatic Calculus for Boolean Satisfiability

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Gu, Tao Piedeleu, Robin Zanasi, Fabio University College London United Kingdom

We propose a calculus of string diagrams to reason about satisfiability of Boolean formulas, and prove it to be sound and complete. We then showcase our calculus in a few case studies. First, we consider SAT-solving. Second, we consider Horn clauses, which leads us to a new decision method for propositional logic programs equivalence under Herbrand model semantics. © 2022, CC BY.

关键词： logic programming

On the integration of declarative choreographies and Commitment-based agent societies into the SCIFF logic programming framework

学校读者我要写书评

暂无评论

On the integration of declarative choreographies and Commitm...

作者： Chesani, Federico Mello, Paola Montali, Marco Storari, Sergio Torroni, Paolo DEIS University of Bologna viale Risorgimento 2 Bologna40136 Italy ENDIF University of Ferrara Via Saragat 1 Ferrara44100 Italy

The definition of choreography specification languages for Service Oriented Systems poses important challenges. Mainstream approaches tend to focus on procedural aspects, leading to over-constrained and over-specified models. Because of such a drawback, declarative languages are gaining popularity as a better way to model service choreographies. A similar issue was met in the Multi-Agent Systems domain, where declarative approaches based on social semantics have been used to capture the nature of agent interaction without over-constraining their behaviour. In this work, we present an integrated framework capable to cover the entire cycle of specification and verification of choreographies, by mixing approaches coming from the Service Oriented Computing and Multi-Agent Systems research domains. SCIFF is the underlying logic programming framework for modelling and verifying interaction in open systems. The use of SCIFF brings us two main advantages: (1) it allows us to capture within a single framework different aspects of a choreography, ranging from constraints on the flow of messages to effects and commitments resulting from their exchange;(2) it provides an operational model that can be exploited to perform a variety of verification tasks.

关键词： logic programming

ACTION LANGUAGES BASED ACTUAL CAUSALITY FOR COMPUTATIONAL ETHICS: A SOUND AND COMPLETE IMPLEMENTATION IN ASP

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Sarmiento, Camilo Inoue, Katsumi Bourgne, Gauvain Cavalli, Daniele Ganascia, Jean-Gabriel Sorbonne Université CNRS LIP6 ParisF-75005 France National Institute of Informatics Tokyo Japan École Normale Supérieure - Université PSL République des savoirs Collège de France CNRS ParisF-75005 France

Although moral responsibility is not circumscribed by causality, they are both closely intermixed. Furthermore, rationally understanding the evolution of the physical world is inherently linked with the idea of causality. Thus, the decision-making applications based on automated planning inevitably have to deal with causality—especially if they consider imputability aspects or integrate references to ethical norms. The many debates around causation in the last decades have shown how complex this notion is and thus, how difficult is its integration with planning. As a result, much of the work in computational ethics relegates causality to the background, despite the considerations stated above. This paper’s contribution is to provide a complete and sound translation into logic programming from an actual causation definition suitable for action languages—this definition is a formalisation of Wright’s NESS test. The obtained logic program allows to deal with complex causal relations. In addition to enabling agents to reason about causality, this contribution specifically enables the computational ethics domain to handle situations that were previously out of reach. In a context where ethical considerations in decision-making are increasingly important, advances in computational ethics can greatly benefit the entire AI community. © 2022, CC BY-SA.

关键词： logic programming

Cosmos: A Comprehensive Framework for Automatically Generating Domain-Oriented Test Suite

学校读者我要写书评

暂无评论

SSRN

SSRN 2022年

作者： Kalaee, Akram Parsa, Saeed Fathi, Negar School of Computer Engineering Iran University of Science and Technology Tehran16846-13114 Iran

Context: Constraint solvers basically attempt to provide test data satisfying a given path constraint. However, a major difficulty is that fault does not reveal in many cases unless the input data fall in a particular ***: This paper introduces the new concept of domain solver, called COSMOS. COSMOS computes the feasible domain of inputs for a given path constraint. Domain coverage is of great use to evaluate the adequacy of test data used to reveal latent faults, particularly where there are coincidentally correct executions. Such executions degrade spectrum-based fault localization ***: COSMOS splits a path constraint into conjunctions of comparisons. Such a splitting simplifies the constraint solving task to find the regions satisfying a comparison between two expressions of compatible types. After finding a region satisfying a comparison between two expressions, an improved version of an algorithm, update, is used to determine the domain of variables involved in the comparing ***: COSMOS is implemented using the Roslyn compiler and assessed the benefits and costs of our domain solver with some well-known constraint solvers such as CVC4, Yices2, and Z3. Our experiments with an industrial benchmark with 55 constraints show that Domain-solver improves the number of supported data types involved in a constraint and solves100\% of the instances on which the other solvers fail. It also achieves the best accuracy of 84\% compared to existing domain-oriented test suite generation approaches, such as PRT, IP-PRT, DDR, and ***: In comparison with the existing domain-oriented test suite generation methods, COSMOS supports a wide range of data types, from basic to complex. COSMOS generates more accurate subdomains in the desired time than the domain-oriented test suite generation methods. COSMOS is also more effective than the selected constraint solvers in terms of the number of solved constraints. © 2022, The Authors

关键词： logic programming

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses

学校读者我要写书评

暂无评论

arXiv 2022年

作者： de Angelis, Emanuele Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio IASI-CNR Rome Italy University of Chieti-Pescara Pescara Italy University of Rome ‘Tor Vergata’ Rome Italy

We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs) by which the verification problem is reduced to the problem of checking satisfiability of a set of clauses derived from the given program and contracts. We consider programs that manipulate algebraic data types (ADTs) and a class of contracts specified by catamorphisms, that is, functions defined by simple recursion schemata on the given ADTs. We show by several examples that state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problems obtained by direct translation of the contracts into CHCs. To overcome this difficulty, we propose a transformation technique that removes the ADT terms from CHCs and derives new sets of clauses that work on basic sorts only, such as integers and booleans. Thus, when using the derived CHCs there is no need for induction rules on ADTs. We prove that the transformation is sound, that is, if the derived set of CHCs is satisfiable, then so is the original set. We also prove that the transformation always terminates for the class of contracts specified by catamorphisms. Finally, we present the experimental results obtained by an implementation of our technique when verifying many non-trivial contracts for ADT manipulating programs. Copyright © 2022, The Authors. All rights reserved.

关键词： logic programming

Instrumenting Microservices for Concurrent Audit Logging: Beyond Horn Clauses

学校读者我要写书评

暂无评论

Instrumenting Microservices for Concurrent Audit Logging: Be...

IEEE Annual International Computer Software and Applications Conference (COMPSAC)

作者： Nicolas D. Ahn Sepehr Amir– Mohammadian Dept. of Computer Science University of the Pacific Stockton CA USA

ISBN: (数字)9781665488105

ISBN: (纸本)9781665488112

Instrumenting legacy code is an effective approach to enforce security policies. Formal correctness of this approach in the realm of audit logging relies on semantic frameworks that leverage information algebra to model and compare the information content of the generated audit logs and the program at runtime. Previous work has demonstrated the applicability of instrumentation techniques in the enforcement of audit logging policies for systems with microservices architecture. However, the specified policies suffer from the limited expressivity power as they are confined to Horn clauses being directly used in logic programming engines. In this paper, we explore audit logging specifications that go beyond Horn clauses in certain aspects, and the ways in which these specifications are automatically enforced in microservices. In particular, we explore an instrumentation tool that rewrites Java-based microservices according to a JSON specification of audit logging requirements, where these logging requirements are not limited to Horn clauses. The rewritten set of microservices are then automatically enabled to generate audit logs that are shown to be formally correct.

关键词： Java Codes Runtime logic programming Instruments Semantics Microservice architectures