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

丛书名： Lecture Notes in Computer Science

1000年

作者： Rupak Majumdar Viktor Kunčak

the two-volume set LNCS 10426 and LNCS 10427 constitutes the refereed proceedings of the 29th international conference on Computer Aided Verification, CAV 2017, held in Heidelberg, Germany, in July 2017.

ISBN: (数字)9783319633909

ISBN: (纸本)9783319633893

关键词： logics and Meanings of Programs programming Languages, Compilers, Interpreters Software Engineering programming Techniques Computing Milieux Mathematical logic and Formal Languages

来源：评论

学校读者我要写书评

暂无评论

Answer set programming as a modeling language for course timetabling

引用

thEORY AND PRACTICE OF logic programming 2013年第4-5期13卷 783-798页

作者： Banbara, Mutsunori Soh, Takehide Tamura, Naoyuki Inoue, Katsumi Schaub, Torsten Kobe Univ Nada Ku Kobe Hyogo 6578501 Japan Res Org Informat & Syst Natl Inst Informat Chiyoda Ku Tokyo 1018430 Japan Univ Potsdam D-14482 Potsdam Germany

the course timetabling problem can be generally defined as the task of assigning a number of lectures to a limited set of timeslots and rooms, subject to a given set of hard and soft constraints. the modeling language for course timetabling is required to be expressive enough to specify a wide variety of soft constraints and objective functions. Furthermore, the resulting encoding is required to be extensible for capturing new constraints and for switching them between hard and soft, and to be flexible enough to deal with different formulations. In this paper, we propose to make effective use of ASP as a modeling language for course timetabling. We show that our ASP-based approach can naturally satisfy the above requirements, through an ASP encoding of the curriculum-based course timetabling problem proposed in the third track of the second international timetabling competition (ITC-2007). Our encoding is compact and human-readable, since each constraint is individually expressed by either one or two rules. Each hard constraint is expressed by using integrity constraints and aggregates of ASP. Each soft constraint S is expressed by rules in which the head is the form of penalty (S, V, C), and a violation V and its penalty cost C are detected and calculated respectively in the body. We carried out experiments on four different benchmark sets with five different formulations. We succeeded either in improving the bounds or producing the same bounds for many combinations of problem instances and formulations, compared with the previous best known bounds.

关键词： answer set programming educational timetabling course timetabling

来源：评论

学校读者我要写书评

暂无评论

A practical analysis of non-termination in large logic programs

引用

thEORY AND PRACTICE OF logic programming 2013年第4-5期13卷 705-719页

作者： Liang, Senlin Kifer, Michael SUNY Stony Brook Dept Comp Sci Stony Brook NY USA

A large body of work has been dedicated to termination analysis of logic programs but relatively little has been done to analyze non-termination. In our opinion, explaining non-termination is a much more important task because it can dramatically improve a user's ability to effectively debug large, complex logic programs without having to abide by punishing syntactic restrictions. Non-termination analysis examines program execution history when the program is suspected to not terminate and informs the programmer about the exact reasons for this behavior. In Liang and Kifer (2013), we studied the problem of non-termination in tabled logic engines with subgoal abstraction, such as XSB, and proposed a suite of algorithms for non-termination analysis, called Terminyzer. these algorithms analyze forest logging traces and output sequences of tabled subgoal calls that are the likely causes of non-terminating cycles. However, this feedback was hard to use in practice: the same subgoal could occur in multiple rule heads and in even more places in rule bodies, so Terminyzer left too much tedious, sometimes combinatorially large amount of work for the user to do manually. Here we propose a new suite of algorithms, Terminyzer(+), which closes this usability gap. Terminyzer+ can detect not only sequences of subgoals that cause non-termination, but, importantly, the exact rules where they occur and the rule sequences that get fired in a cyclic manner, thus causing non-termination. this makes Terminyzer(+) suitable as a back-end for user-friendly graphical interfaces on top of Terminyzer(+), which can greatly simplify the debugging process. Terminyzer(+) back-ends exist for the SILK system as well as for the open-source Flora-2 system. A graphical interface has been developed for SILK and is currently underway for Flora-2. We also report experimental studies, which confirm the effectiveness of Terminyzer(+) on a host of large real-world knowledge bases. All tests used in this pape

关键词： terminyzer termination and non-termination analysis logic programming

来源：评论

学校读者我要写书评

暂无评论

SeaLion: An eclipse-based IDE for answer-set programming with advanced debugging support

引用

thEORY AND PRACTICE OF logic programming 2013年第4-5期13卷 657-673页

作者： Busoniu, Paula-Andra Oetsch, Johannes Puehrer, Joerg Skocovsky, Peter Tompits, Hans Vienna Univ Technol Inst Informat Syst 184 3 A-1040 Vienna Austria Univ Nova Lisboa CENTRIA P-2829516 Caparica Portugal Dept Informat P-2829516 Caparica Portugal

In this paper, we present SeaLion, an integrated development environment (IDE) for answer-set programming (ASP). SeaLion provides source-code editors for the languages of Gringo and DLV and offers popular amenities like syntax highlighting, syntax checking, code completion, visual program outline, and refactoring functionality. the tool has been realised in the context of a research project whose goal is the development of techniques to support the practical coding process of answer-set programs. In this respect, SeaLion is the first IDE for ASP that provides debugging features that work for real-world answer-set programs and supports the rich languages of modern answer-set solvers. Indeed, SeaLion implements a stepping-based debugging approach that allows the developer to quickly track down programming errors by simply following his or her intuitions on the intended semantics. Besides that, SeaLion supports ASP development using model-driven engineering techniques including domain modelling with extended UML class diagrams and visualisation of answer sets in corresponding instance diagrams. Moreover, customised visualisation as well as visual editing of answer sets is realised by the Kara plugin of SeaLion. Further implemented features are a documentation generator based on the LANA annotation language, support for external solvers, and interoperability with external tools. SeaLion comes as a plugin of the popular Eclipse platform and provides interfaces for future extensions of the IDE.

关键词： Visualization programming Answer research project IDE Debugging Language

来源：评论

学校读者我要写书评

暂无评论

An Instance Based Model for Scalable θ-Subsumption

引用

international JOURNAL ON ARTIFICIAL INTELLIGENCE TOOLS 2018年第7期27卷

作者： Leger, Hippolyte Bouthinon, Dominique Lebbah, Mustapha Azzag, Hanene Univ Paris 13 LIPN UMR CNRS 7030 99 Ave Jean Baptiste Clement F-93430 Villetaneuse France

the theta-subsumption test is known to be a bottleneck in inductive logic programming. the state-of-the-art learning systems in this field are hardly scalable. Last year, we have created a distributed theta-subsumption process based on an Actor Model, with the aim of being able to decide subsumption on very large clauses. this model was correct and complete, but was also very slow. this is why we introduce ANTS (Actor Network based theta-Subsumption), a new model also based on an actor network, which is significantly faster than the previous one.

关键词： theta-subsumption inductive logic programming actor model distributed computing Akka

来源：评论

学校读者我要写书评

暂无评论

Stable model semantics for founded bounds

Stable model semantics for founded bounds

引用

29th international conference on logic programming ICLP

作者： Aziz, Rehan Abdul Chu, Geoffrey Stuckey, Peter J. Univ Melbourne Dept Comp & Informat Syst Victoria Lab Natl ICT Australia Melbourne Vic 3010 Australia

Answer Set programming (ASP) is a powerful form of declarative programming used in areas such as planning or reasoning. ASP solvers enforce stable model semantics, which rule out solutions representing certain kinds of circular reasoning. Unfortunately, current ASP solvers are incapable of solving problems involving cyclic dependencies between multiple integer or continuous quantities effectively. In this paper, we generalize the notion of stable models to bound founded variables with arbitrary domains, where bounds on such variables need to be justified by some rule in the program in order for the model to be stable. We show how to handle significantly more general rule forms where bound founded variables can act as head or body variables, and where head and body variables can be related via complex constraints subject to certain monotonicity requirements. We describe a new unfounded set detection algorithm which allows us to enforce this generalization of the stable model semantics. We also show how these unfounded sets can be explained in order to allow effective conflict-directed clause learning. the new solver merges the best features of CP, SAT and ASP solvers and allows new types of problems to be solved very efficiently.

关键词： answer set programming stable model semantics finite domain solving

来源：评论

学校读者我要写书评

暂无评论

A functional view of strong negation in answer set programming 6

A functional view of strong negation in answer set programmi...

引用

6th Workshop on Answer Set programming and Other Computing Paradigms, ASPOCP 2013, co-located with the 29th international conference on logic programming, ICLP 2013

作者： Bartholomew, Michael Lee, Joohyung School of Computing Informatics Decision Systems Engineering Arizona State University Tempe United States

the distinction between strong negation and default negation has been useful in answer set programming. We present an alternative account of strong negation, which lets us view strong negation in terms of the functional stable model semantics by Bartholomew and Lee. More specifically, we show that, under complete interpretations, minimizing both positive and negative literals in the traditional answer set semantics is essentially the same as ensuring the uniqueness of Boolean function values under the functional stable model semantics. the same account lets us view Lifschitz’s two-valued logic programs as a special case of the functional stable model semantics. In addition, we show how non-Boolean intensional functions can be eliminated in favor of Boolean intensional functions, and furthermore can be represented using strong negation, which provides a way to compute the functional stable model semantics using existing ASP solvers. We also note that similar results hold with the functional stable model semantics by Cabalar. © 2013 ***. All rights reserved.

关键词： Boolean functions

来源：评论

学校读者我要写书评

暂无评论

Rational closure for all description logics 29

Rational closure for all description logics

引用

29th international Joint conference on Artificial Intelligence, IJCAI 2020

作者： Bonatti, Piero A. Università di Napoli Federico II Italy

ISBN: (纸本)9780999241165

Many modern applications of description logics (DLs, for short), such as biomedical ontologies and semantic web policies, provide compelling motivations for extending DLs with an overriding mechanism analogous to the homonymous feature of object-oriented programming. Rational closure (RC) is one of the candidate semantics for such extensions, and one of the most intensively studied. So far, however, it has been limited to strict fragments of SROIQ(D) - the logic on which OWL2 is founded. In this paper we prove that RC cannot be extended to logics that do not satisfy the disjoint model union property, including SROIQ(D). then we introduce a refinement of RC called stable rational closure that overcomes the dependency on the disjoint model union property. Our results show that stable RC is a natural extension of RC. However, its positive features come at a price: stable RC re-introduces one of the undesirable features of other nonmonotonic logics, namely, deductive closures may not exist and may not be unique. © 2020 Inst. Sci. inf., Univ. Defence in Belgrade. All rights reserved.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

29th international conference on Computer Aided Verification, CAV 2017

29th International Conference on Computer Aided Verification...

引用

29th international conference on Computer Aided Verification, CAV 2017

ISBN: (纸本)9783319633893

the proceedings contain 61 papers. the special focus in this conference is on Computer Aided Verification. the topics include: Verified compilation of space-efficient reversible circuits;ascertaining uncertainty for efficient exact cache analysis;non-polynomial worst-case analysis of recursive programs;decorated-component-based program synthesis;electrical bug localization during post-silicon validation enabled by quick error detection and formal methods;efficient parallel strategy improvement for parity games;model-checking linear-time properties of parametrized asynchronous shared memory pushdown systems;minimization of symbolic transducers;abstract interpretation with unfoldings;cutoff bounds for consensus algorithms;towards verifying nonlinear integer arithmetic;network-wide configuration synthesis;verifying equivalence of spark programs;synchronization synthesis for network programs;an experimentation framework for bounded synthesis;quantitative assume guarantee synthesis;syntax-guided optimal synthesis for chemical reaction networks;model counting for recursively-defined strings;a three-tier strategy for reasoning about floating-point numbers in SMT;a correct-by-decision solution for simultaneous place and route;on expansion and resolution in CEGAR based QBF solving;a decidable fragment in separation logic with inductive predicates and arithmetic;finding fix locations for CFL reachability analyses via minimum cuts;proving linearizability using forward simulations;automating induction for solving horn clauses and on multiphase-linear ranking functions.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Explainability via Short Formulas: the Case of Propositional logic with Implementation 1

Explainability via Short Formulas: the Case of Propositional...

引用

1st international Workshop on HYbrid Models for Coupling Deductive and inductive ReAsoning and the 29th RCRA Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, HYDRA-RCRA 2022

作者： Jaakkola, Reijo Janhunen, Tomi Kuusisto, Antti Rankooh, Masood Feyzbakhsh Vilander, Miikka Tampere University FI-33014 Finland

We conceptualize explainability in terms of logic and formula size, giving a number of related definitions of explainability in a very general setting. Our main interest is the so-called special explanation problem which aims to explain the truth value of an input formula in an input model. the explanation is a formula of minimal size that (1) agrees with the input formula on the input model and (2) transmits the involved truth value to the input formula globally, i.e., on every model. As an important example case, we study propositional logic in this setting and show that the special explainability problem is complete for the second level of the polynomial hierarchy. We also provide an implementation of this problem in answer set programming and investigate its capacity in relation to explaining answers to the n-queens and dominating set problems. © 2022 Copyright for this paper by its authors.

关键词： Computer circuits

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：