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

On the Configuration of More and Less Expressive logic Programs

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Dodaro, Carmine Maratea, Marco Vallati, Mauro University of Calabria Italy University of Genoa Italy University of Huddersfield United Kingdom

The decoupling between the representation of a certain problem, i.e., its knowledge model, and the reasoning side is one of main strong points of model-based Artificial Intelligence (AI). This allows, e.g. to focus on improving the reasoning side by having advantages on the whole solving process. Further, it is also well-known that many solvers are very sensitive to even syntactic changes in the input. In this paper, we focus on improving the reasoning side by taking advantages of such sensitivity. We consider two well-known model-based AI methodologies, SAT and ASP, define a number of syntactic features that may characterise their inputs, and use automated configuration tools to reformulate the input formula or program. Results of a wide experimental analysis involving SAT and ASP domains, taken from respective competitions, show the different advantages that can be obtained by using input reformulation and configuration. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2022, The Authors. All rights reserved.

关键词： logic programming

programming model for concept learning and its solution based on genetic algorithms

学校读者我要写书评

暂无评论

Programming model for concept learning and its solution base...

3rd World Congress on Intelligent Control and Automation

作者： Li, MQ Kou, JS Zhou, J Tianjin Univ Inst Syst Engn Tianjin 300072 Peoples R China

ISBN: (纸本)7312012035

Learning from examples is an important branch of inductive learning, and is also the bottle-neck in concepts extraction of machine learning. Based on inductive learning theory, this paper applies combinatorial optimization method to setup the programming models of learning concepts of the prepositional logic formulas in the conjunctive normal form (CNF) and disjunctive normal form (DNF). Then, genetic algorithms (GA), specified to CNF learning, is designed. GA can find the multiple optimal solution in theory and practice, and experiments reveal that it runs more efficiently compared with heuristic algorithms of the GS type.

关键词： inductive learning programming model knowledge acquisition genetic algorithms

Completing the Picture: Complexity of Graded Modal logics with Converse

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Bednarczyk, Bartosz Kieronski, Emanuel Witkowski, Piotr Institute of Computer Science University of Wroclaw Poland and Computational Logic Group TU Dresden Germany Institute of Computer Science University of Wroclaw Poland

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames have already been established. By"traditional" classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

CNL2ASP: converting controlled natural language sentences into ASP

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Caruso, Simone Dodaro, Carmine Maratea, Marco Mochi, Marco Riccio, Francesco DIBRIS University of Genova Genova Italy DeMaCS University of Calabria Rende Italy Engineering Division ALTEN Italia Torino Italy

Answer Set programming (ASP) is a popular declarative programming language for solving hard combinatorial problems. Although ASP has gained widespread acceptance in academic and industrial contexts, there are certain user groups who may find it more advantageous to employ a higher-level language that closely resembles natural language when specifying ASP programs. In this paper, we propose a novel tool, called CNL2ASP, for translating English sentences expressed in a controlled natural language (CNL) form into ASP. In particular, we first provide a definition of the type of sentences allowed by our CNL and their translation as ASP rules, and then exemplify the usage of the CNL for the specification of both synthetic and real-world combinatorial problems. Finally, we report the results of an experimental analysis conducted on the real-world problems to compare the performance of automatically generated encodings with the ones written by ASP practitioners, showing that our tool can obtain satisfactory performance on these benchmarks. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2023, The Authors. All rights reserved.

关键词： logic programming

Technical note the external interface for extending WASP

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Dodaro, Carmine Ricca, Francesco DIBRIS University of Genova Genova Italy DEMACS University of Calabria Rende Italy

Answer set programming (ASP) is a successful declarative formalism for knowledge representation and reasoning. The evaluation of ASP programs is nowadays based on the Conflict-Driven Clause Learning (CDCL) backtracking search algorithm. Recent work suggested that the performance of CDCL-based implementations can be considerably improved on specific benchmarks by extending their solving capabilities with custom heuristics and propagators. However, embedding such algorithms into existing systems requires expert knowledge of the internals of ASP implementations. The development of effective solver extensions can be made easier by providing suitable programming interfaces. In this paper, we present the interface for extending the CDCL-based ASP solver WASP. The interface is both general, i.e. it can be used for providing either new branching heuristics and propagators, and external, i.e. the implementation of new algorithms requires no internal modifications of WASP. Moreover, we review the applications of the interface witnessing it can be successfully used to extend WASP for solving effectively hard instances of both real-world and synthetic problems. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Symbolic Specialization of Rewriting logic Theories with Presto

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Alpuente, María Escobar, Santiago Sapiña, Julia Ballis, Demis Universitat Politècnica de València Spain DMIF University of 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. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2021, The Authors. All rights reserved.

关键词： Algebra

学校读者我要写书评

暂无评论

用于验证多智能体系统的APTL模型检测器

软件学报 2019年第2期30卷 231-243页

作者：王海洋段振华田聪西安电子科技大学计算理论与技术研究所陕西西安710071 综合业务网理论及关键技术国家重点实验室(西安电子科技大学) 陕西西安710071

由于经典的线性时序逻辑表达能力有限,设计并开发了基于交替投影时序逻辑(alternating projection temporal logic,简称APTL)的模型检测工具.根据王海洋等人提出的APTL符号模型检测方法,设计并实现了APTL模型检测器MCMAS_APTL.该工具可... 详细信息

由于经典的线性时序逻辑表达能力有限,设计并开发了基于交替投影时序逻辑(alternating projection temporal logic,简称APTL)的模型检测工具.根据王海洋等人提出的APTL符号模型检测方法,设计并实现了APTL模型检测器MCMAS_APTL.该工具可用于多智能体系统(multi-agent system,简称MAS)的性质验证.MCMAS_APTL检查MAS是否满足具体性质的过程如下:首先,用解释系统编程语言(interpreted system programming language,简称ISPL)描述要验证的系统IS,用APTL公式P描述要验证的性质;然后,符号化表示系统IS,并将非P转化为范式;最后,计算所有满足非P的路径的起始状态集合.如果得到的状态集合中包含系统的初始状态,则说明系统不满足公式P;反之,则说明系统满足公式P.详细阐述了实现MCMAS_APTL的过程,并且通过验证机器人足球赛的例子展示了MCMAS_APTL的性能.

关键词：交替投影时序逻辑多智能体系统模型检测

CASP solutions for planning in hybrid domains

学校读者我要写书评

暂无评论

arXiv 2017年

作者： Balduccini, Marcello Magazzeni, Daniele Maratea, Marco Leblanc, Emily C. Saint Joseph's University United States King's College London United Kingdom University of Genoa Italy Drexel University United States

CASP is an extension of ASP that allows for numerical constraints to be added in the rules. PDDL+ is an extension of the PDDL standard language of automated planning for modeling mixed discrete-continuous dynamics. In this paper, we present CASP solutions for dealing with PDDL+ problems, i.e., encoding from PDDL+ to CASP, and extensions to the algorithm of the ezcsp CASP solver in order to solve CASP programs arising from PDDL+ domains. An experimental analysis, performed on well-known linear and non-linear variants of PDDL+ domains, involving various configurations of the ezcsp solver, other CASP solvers, and PDDL+ planners, shows the viability of our solution. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2017, The Authors. All rights reserved.

关键词： logic programming

On relation between constraint answer set programming and satisfiability modulo theories

学校读者我要写书评

暂无评论

arXiv 2017年

作者： Lierler, Yuliya Susman, Benjamin Department of Computer Science University of Nebraska at Omaha OmahaNB68182 United States

Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiabilitymodulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will booster the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs. Under consideration in theory and practice of logic programming (TPLP). Copyright © 2017, The Authors. All rights reserved.

关键词： Integer programming