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

Stepping through an Answer-Set Program

11th international conference on logic programming and nonmonotonic reasoning (lpnmr)

作者： Oetsch, Johannes Puehrer, Joerg Tompits, Hans Vienna Univ Technol Inst Informat Syst 184 3 A-1040 Vienna Austria

ISBN: (纸本)9783642208942

We introduce a framework for interactive stepping through an answer-set program as a means for debugging. In procedural languages, stepping is a widespread and effective debugging strategy. the idea is to gain insight into the behaviour of a program by executing statement by statement, following the program's control flow. Stepping has not been considered for answer-set programs so far, presumably because of their lack of a control flow. the framework we provide allows for stepwise constructing interpretations following the user's intuition on which rule instances to become active. that is, we do not impose any ordering on the rules but give the programmer the freedom to guide the stepping process. Due to simple syntactic restrictions, each step results in a state that guarantees stability of the intermediate interpretation. We present how stepping can be started from breakpoints as in conventional programming and discuss how the approach can be used for debugging using a running example.

关键词： answer-set programming program analysis debugging

来源：评论

学校读者我要写书评

暂无评论

Induction on Failure: Learning Connected Horn theories

引用

10th international conference on logic programming and nonmonotonic reasoning

作者： Kimber, Tim Broda, Krysia Russo, Alessandra Univ London Imperial Coll Sci Technol & Med London SW7 2AZ England

ISBN: (纸本)9783642042379

Several learning systems based on Inverse Entailment (IE) have been proposed, some that compute single clause hypotheses, exemplified by Progol, and others that, produce multiple clauses in response to a single seed example. A common denominator of these systems, is a restricted hypothesis search space, within which each clause must individually explain some example E, or some member of an abductive explanation for E. this paper proposes a new IE approach, called Induction on Failure (IoF), that generalises existing Horn clause learning systems by allowing the computation of hypotheses within a larger search space, namely that of Connected theories. A proof procedure for IoF is proposed that generalises existing IE systems and also resolves Yamamoto's example. A prototype implementation is also described. Finally, a semantics is presented called Connected theory Generalisation, which is proved to extend Kernel Set Subsumption and to include hypotheses constructed within this new IoF approach.

关键词： Inductive logic programming Inverse Entailment Abduction

来源：评论

学校读者我要写书评

暂无评论

A General Approach to the Verification of Cryptographic Protocols Using Answer Set programming

引用

10th international conference on logic programming and nonmonotonic reasoning

作者： Delgrande, James P. Grote, Torsten Hunter, Aaron Simon Fraser Univ Sch Comp Sci Burnaby BC V5A 1S6 Canada

ISBN: (纸本)9783642042379

We introduce a general approach to cryptographic protocol verification based oil answer set programming. In our approach, cryptographic protocols are represented as extended logic programs where the answer Sets correspond to traces of protocol runs. Using queries, we can find attacks on a protocol by finding the answer sets for the corresponding logic program. Our encoding is modular, with different modules representing the message passing environment, the protocol Structure and the intruder model. We can easily tailor each module to suit a specific application, while keeping the rest of the encoding constant. As such. our approach is more flexible and elaboration tolerant than related formalizations. the present system is intended as a first step towards the development of a compiler from protocol specifications to executable programs: such a compiler would make verification a completely automated process. this work is also part of a larger project in which we are exploring the advantages of explicit, declarative representations of protocol verification problems.

关键词： Message passing

来源：评论

学校读者我要写书评

暂无评论

Splitting and updating hybrid knowledge bases

引用

thEORY AND PRACTICE OF logic programming 2011年第4-5期11卷 801-819页

作者： Slota, Martin Leite, Joao Swift, Terrance Univ Nova Lisboa CENTRIA P-2829516 Caparica Portugal Univ Nova Lisboa Dept Informat P-2829516 Caparica Portugal

Over the years, nonmonotonic rules have proven to be a very expressive and useful knowledge representation paradigm. they have recently been used to complement the expressive power of Description logics (DLs), leading to the study of integrative formal frameworks, generally referred to as hybrid knowledge bases, where both DL axioms and rules can be used to represent knowledge. the need to use these hybrid knowledge bases in dynamic domains has called for the development of update operators, which, given the substantially different way DLs and rules are usually updated, has turned out to be an extremely difficult task. In Slota and Leite (2010b Towards Closed World reasoning in Dynamic Open Worlds. theory and Practice of logic programming, 26th Int'l. conference on logic programming (ICLP'10) Special Issue 10(4-6) (July), 547-564.), a first step towards addressing this problem was taken, and an update operator for hybrid knowledge bases was proposed. Despite its significance-not only for being the first update operator for hybrid knowledge bases in the literature, but also because it has some applications-this operator was defined for a restricted class of problems where only the ABox was allowed to change, which considerably diminished its applicability. Many applications that use hybrid knowledge bases in dynamic scenarios require both DL axioms and rules to be updated. In this paper, motivated by real world applications, we introduce an update operator for a large class of hybrid knowledge bases where both the DL component as well as the rule component are allowed to dynamically change. We introduce splitting sequences and splitting theorem for hybrid knowledge bases, use them to define a modular update semantics, investigate its basic properties, and illustrate its use on a realistic example about cargo imports.

关键词： Hybrid knowledge base Update Splitting theorem Ontology logic program

来源：评论

学校读者我要写书评

暂无评论

Metric Temporal Answer Set programming over Timed Traces 16th

Metric Temporal Answer Set Programming over Timed Traces

引用

16th international conference on logic programming and Non-Monotonic reasoning (lpnmr)

作者： Cabalar, Pedro Dieguez, Martin Schaub, Torsten Schuhmann, Anna Univ A Coruna Coruna Spain Univ Angers LERIA Angers France Univ Potsdam Potsdam Germany

ISBN: (纸本)9783031157073;9783031157066

In temporal extensions of Answer Set programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. In many applications, however, timing constraints are important like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. the resulting Metric Equilibrium logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium logic and Monadic Quantified Equilibrium logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Cc Τ on stage: Generalised uniform equivalence testing for verifying student assignment solutions

引用

10th international conference on logic programming and nonmonotonic reasoning, lpnmr 2009

作者： Oetsch, Johannes Seidl, Martina Tompits, Hans Woltran, Stefan Institut für Informationssysteme Technische Universität Wien Favoritenstrae 9-11 A-1040 Vienna Austria Institut für Softwaretechnik Technische Universität Wien Favoritenstrae 9-11 A-1040 Vienna Austria

ISBN: (纸本)3642042376

the tool cc Τ is an implementation for testing various parameterised notions of program correspondence between logic programs under the answer-set semantics, based on reductions to quantified propositional logic. One such notion is relativised uniform equivalence with projection, which extends standard uniform equivalence via two additional parameters: one for specifying the input alphabet and one for specifying the output alphabet. In particular, the latter parameter is used for projecting answer sets to the set of designated output atoms, i.e. ignoring auxiliary atoms during answer-set comparison. In this paper, we discuss an application of cc Τ for verifying the correctness of students' solutions drawn from a laboratory course on logic programming, employing relativised uniform equivalence with projection as the underlying program correspondence notion. We complement our investigation by discussing a performance evaluation of cc Τ, showing that discriminating among different back-end solvers for quantified propositional logic is a crucial issue towards optimal performance. © 2009 Springer Berlin Heidelberg.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Manifold Answer-Set Programs for Meta-reasoning

引用

10th international conference on logic programming and nonmonotonic reasoning

作者： Faber, Wolfgang Woltran, Stefan Univ Calabria I-87030 Commenda Di Rende Italy Vienna Univ Technol A-1040 Vienna Austria

ISBN: (纸本)9783642042379

In answer-set programming (ASP), the main focus usually is on computing answer sets which correspond to solutions to the problem represented by a logic program. Simple reasoning over answer sets is sometimes supported by ASP systems (usually in the form of computing brave or cautious consequences), but Slightly more involved reasoning problems require external postprocessing. Generally speaking, it is often desirable to use (a subset of) brave or cautious consequences of a program P-1 as input to another program P-2 in order to provide the desired Solutions to the problem to be solved. In practice, the evaluation of the program P-1 Currently has to be decopuled from the evaluation of P-2 using an intermediate step which collects the desired consequences of P-1 and provides them as input to P-2. In this work, we present a novel method for representing such a procedure within a single program, and thus within the realm of ASP itself. Our technique relies oil rewriting P-1 into a so-called manifold program. which allows for accessing all desired consequences of P-1 within a single answer set. then, this manifold program can be evaluated jointly with P-2 avoiding any intermediate computation step. For determining the consequences within the manifold program we use weak constraints, which is strongly motivated by complexity considerations. As an application, we present all encoding for computing the ideal extension of,in abstract argumentation framework.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Magic Sets for the Bottom-Up Evaluation of Finitely Recursive Programs

引用

10th international conference on logic programming and nonmonotonic reasoning

作者： Calimeri, Francesco Cozza, Susanna Ianni, Giovambattista Leone, Nicola Univ Calabria Dept Math I-87036 Arcavacata Di Rende CS Italy

ISBN: (纸本)9783642042379

the support for function symbols in logic programming under answer set semantics allows to overcome some modeling limitations of traditional Answer Set programming (ASP) systems, Such as the inability of handling infinite domains. On the other hand, admitting function symbols in ASP makes inference undecidable in the general case. Lately. the research community is focusing on finding proper subclasses for which decidability of inference is guaranteed. the two major proposals, so far, are finitary programs and finitely-ground programs. these two proposals are somehow complementary: indeed, the former is conceived to allow decidable querying (by means of a top-down evaluation strategy), while file latter supports the computability of answer-sets (by means of a bottom-up evaluation strategy). One of the main advantages of finitely-ground programs is that they can be "directly" evaluated by Current ASP systems, which are based on a bottom-up computational model. However, there are also some interesting programs which are suitable for top-down query evaluation;but do not fall in the class of finitely-ground programs. In this paper, we focus on disjunctive finitely-recursive Positive (DFRP) programs. We present a proper adaptation of the magic-sets technique for DFRP programs, which ensures query equivalence under both brave and cautious reasoning. We show that, if the input program is DFRP, then its magic-set rewriting is guaranteed to be finitely ground. thus, reasoning oil DFRP programs turns Out to be decidable, and we provide an effective method for its computation on the ASP system DLV.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

VIDEAS: A Development Tool for Answer-Set Programs Based on Model-Driven Engineering Technology

引用

11th international conference on logic programming and nonmonotonic reasoning (lpnmr)

作者： Oetsch, Johannes Puehrer, Joerg Seidl, Martina Tompits, Hans Zwickl, Patrick Vienna Univ Technol Inst Informat Syst 184 3 Favoritenstr 9-11 A-1040 Vienna Austria Johannes Kepler Univ Linz Inst Formale Modelle & Verifikat A-4040 Linz Austria Tech Univ Inst Softwaretech Vienna Austria FTW Forschungszentrum Telekommunikat Wien GmbH A-1220 Vienna Austria

ISBN: (纸本)9783642208942;9783642208959

In the object-oriented world, much effort is spent into the development of dedicated tools to ease programming and to prevent programming errors. Recently, the techniques of model-driven engineering (MDE) have been proven especially valuable to manage the complexity of modern software systems during the software development process. In the world of answer-set programming (ASP), the situation is different. Much effort is invested into the development of efficient solvers, but the pragmatics of programming itself has not received much attention and more tool support to ease the actual programming phase would be desirable. To address this issue, we introduce the tool VIDEAS which graphically supports the partial specification of answer-set programs, applying technologies provided by MDE.

关键词： answer-set programming model-driven engineering ER diagrams

来源：评论

学校读者我要写书评

暂无评论

A Default Approach to Semantics of logic Programs with Constraint Atoms

引用

10th international conference on logic programming and nonmonotonic reasoning

作者： Shen, Yi-Dong You, Jia-Huai Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing 100190 Peoples R China Univ Alberta Dept Comp Sci Edmonton T6G 2E8 AB Canada

ISBN: (纸本)9783642042379

We define the semantics of logic programs with (abstract) constraint atoms in a way closely tied to default logic. Like default logic formulas in rules are evaluated using the classical entailment relation, so a constraint atom can be represented by an equivalent propositional formula. therefore, answer sets are defined in a way closely related to default extensions. the semantics defined this way enjoys two properties generally considered desirable for answer set programming - minimality and derivability. the derivability property is very important because it guarantees free of self-supporting, loops in answer sets. We show that a when restricted to basic logic programs, this semantics agrees with the conditional-satisfaction based semantics. Furthermore, answer sets by the minimal-model based semantics can be recast in our approach. Consequently, the default, approach gives a unifying account of the major existing semantics for logic programs with constraint atoms. this also makes it possible to characterize, in terms of the, minimality mid derivability properties, the precise relationship between them and contrast with others.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：