the proceedings contain 39 papers. the topics discussed include: nonmonotonic reasoning in FLORA-2;data integration and answer set programming;unfounded sets for disjunctive logic programs with arbitrary aggregates;on...
详细信息
ISBN:
(纸本)3540285385
the proceedings contain 39 papers. the topics discussed include: nonmonotonic reasoning in FLORA-2;data integration and answer set programming;unfounded sets for disjunctive logic programs with arbitrary aggregates;on modular translations and strong equivalence;guarded open answer set programming;external sources of computation for answer set solvers;answer sets for propositional theories;on the local closed-world assumption of data-sources;game-theoretic reasoning about actions in nonmonotic causal theories;some logical properties of nonmonotic causal theories;solving hard ASP programs efficiently;mode-directed fixed point computation;nested epistemic logic programs;and a social semantics for multi-agent systems.
We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. the central proof-theoretic insights underlying the prover concern resource managem...
详细信息
ISBN:
(纸本)3540280057
We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. the central proof-theoretic insights underlying the prover concern resource management and focused derivations, both of which are traditionally understood in the domain of backward reasoning systems such as logicprogramming. We illustrate how resource management, focusing, and other intrinsic properties of linear connectives affect the basic forward operations of rule application, contraction, and forward subsumption. We also present some preliminary experimental results obtained with our implementation.
We present extended conceptual logic programs (ECLPs), for which reasoning is decidable and, moreover, can be reduced to finite answer set programming. ECLPs are useful to reason with both ontological and rule-based k...
详细信息
We present extended conceptual logic programs (ECLPs), for which reasoning is decidable and, moreover, can be reduced to finite answer set programming. ECLPs are useful to reason with both ontological and rule-based knowledge, which is illustrated by simulating reasoning in an expressive description logic (DL) equipped with DL-safe rules. Furthermore, ECLPs are more expressive in the sense that they enable nonmonotonic reasoning, a desirable feature in locally closed subareas of the Semantic Web.
Trust management is a promising approach for the authorization in distributed environment. there are two key issues for a trust management system: how to design high-level policy language and how to solve the complian...
详细信息
ISBN:
(纸本)3540288953
Trust management is a promising approach for the authorization in distributed environment. there are two key issues for a trust management system: how to design high-level policy language and how to solve the compliance-checking problem [3, 4]. We adopt this approach to deal with distributed authorization with delegation. In this paper, we propose an authorization language AL, a human-understandable high level language to specify various authorization policies. Language AL has rich expressive power which can not only specify delegation, and threshold structures addressed in previous approaches, but also represent structured resources and privileges, positive and negative authorizations, separation of duty, incomplete information reasoning and partial authorization and delegation. We define the semantics of AL through logicprogramming with answer set semantics and through an authorization scenario we demonstrate the application of language AL.
Frequent closed pattern discovery is one of the most important topics in the studies of the compact representation for data mining. In this paper, we consider the frequent closed pattern discovery problem for a class ...
详细信息
ISBN:
(纸本)3540281770
Frequent closed pattern discovery is one of the most important topics in the studies of the compact representation for data mining. In this paper, we consider the frequent closed pattern discovery problem for a class of structured data, called attribute trees (AT), which is a subclass of labeled ordered trees and can be also regarded as a fragment of description logic with functional roles only. We present an efficient algorithm for discovering all frequent closed patterns appearing in a given collection of attribute trees. By using a new enumeration method, called the prefix-preserving closure extension, which enable efficient depth-first search over all closed patterns without duplicates, we show that this algorithm works in polynomial time both in the total size of the input database and the number of output trees generated by the algorithm. To our knowledge, this is one of the first result for output-sensitive algorithms for frequent closed substructure disocvery from trees and graphs.
Cut-elimination is the most prominent form of proof transformation in logic. the elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. the cut-elim...
详细信息
ISBN:
(纸本)3540252363
Cut-elimination is the most prominent form of proof transformation in logic. the elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. the cut-elimination method CERES (cut-elimination by resolution) works by constructing a set of clauses from a proof with cuts. Any resolution refutation of this set can then serve as a skeleton of a proof with only atomic cuts. In this paper we present a systematic experiment withthe implementation of CERES on a proof of reasonable size and complexity. It turns out that the proof with cuts can be transformed into two mathematically different proofs of the theorem. In particular, the application of positive and negative hyperresolution yield different mathematical arguments. As an unexpected side-effect the derived clauses of the resolution refutation proved particularly interesting as they can be considered as meaningful universal lemmas. though the proof under investigation is intuitively simple, the experiment demonstrates that new (and relevant) mathematical information on proofs can be obtained by computational methods. It can be considered as a first step in the development of an experimental culture of computer-aided proof analysis in mathematics.
Two approaches to logicprogramming with probabilities emerged over time: bayesian reasoning and probabilistic satisfiability (PSAT). the attractiveness of the former is in tying the logicprogramming research to the ...
详细信息
We propose a new approach to Inductive logicprogramming i that systematically exploits caching and offers a number of advantages over current systems. It avoids redundant computation, is more amenable to the use of s...
详细信息
the goal of this presentation is to convince the research community that music is much more than an interesting and "nice", but ultimately esoteric toy domain for machine learning experiments. I will try to ...
详细信息
ID-logic uses ideas from the field of logicprogramming to extend second order logic with non-monotone inductive defintions. In this work, we reformulate the semantics of this logic in terms of approximation theory, a...
详细信息
ID-logic uses ideas from the field of logicprogramming to extend second order logic with non-monotone inductive defintions. In this work, we reformulate the semantics of this logic in terms of approximation theory, an algebraic theory which generalizes the semantics of several non-monotonic reasoning formalisms. this allows us to apply certain abstract modularity theorems, developed within the framework of approximation theory, to ID-logic. As such, we are able to offer elegant and simple proofs of generalizations of known theorems, as well as some new results.
暂无评论