reasoning about changes caused by the execution of actions has long been at the center of attention of researchers in the area of logic-based AI. logical properties of causal dependencies turned out to be similar to p...
详细信息
ISBN:
(纸本)9783540738466
reasoning about changes caused by the execution of actions has long been at the center of attention of researchers in the area of logic-based AI. logical properties of causal dependencies turned out to be similar to properties of rules in logic programs. this fact allows us to apply methods of logicprogramming to computational problems related to action and change. Ideas of answer set programming, based on the concept of a stable model, turned out to be particularly useful. In the past they have been applied primarily to the problem of plan generation. there is now increasing interest also in using logicprogramming for learning action descriptions.
the monadic fragments of first-order Godel logics are investigated. It is shown that all finite-valued monadic Godel logics are decidable;whereas, withthe possible exception of one (G(up arrow)), all infinite-valued ...
详细信息
ISBN:
(纸本)9783540755586
the monadic fragments of first-order Godel logics are investigated. It is shown that all finite-valued monadic Godel logics are decidable;whereas, withthe possible exception of one (G(up arrow)), all infinite-valued monadic Godel logics are undecidable. For the missing case G(up arrow) the decidability of an important sub-case, that is well motivated also from an application oriented point of view, is proven. A tight bound for the cardinality of finite models that have to be checked to guarantee validity is extracted from the proof. Moreover, monadic G(up arrow), like all other infinite-valued logics, is shown to be undecidable if the projection operator triangle z, is added, while all finite-valued monadic Godel logics remain decidable with triangle.
this work addresses the issue of prioritized reasoning in the context of logicprogramming. the case of preference conditions involving atoms is considered and a refinement of the comparison method of the ASO semantic...
详细信息
We give the first single-pass ("on the fly") tableau decision procedure for computational tree logic (CTL). Our method extends Schwendimann's single-pass decision procedure for propositional linear tempo...
详细信息
ISBN:
(纸本)9783540755586
We give the first single-pass ("on the fly") tableau decision procedure for computational tree logic (CTL). Our method extends Schwendimann's single-pass decision procedure for propositional linear temporal logic (PLTL) but the extension is non-trivial because of the interactions between the branching inherent in CTL-models, which is missing in PLTL-models, and the "or" branching inherent in tableau search. Our method extends to many other fix-point logics like propositional dynamic logic (PDL) and the logic of common knowledge (LCK). the decision problem for CTL is known to be EXPTIME-complete, but our procedure requires 2EXPTIME in the worst case. A similar phenomenon occurs in extremely efficient practical single-pass tableau algorithms for very expressive description logics with EXPTIME-complete decision problems because the 2EXPTIME worst-case behaviour rarely arises. Our method is amenable to the numerous optimisation methods invented for these description logics and has been implemented in the Tableau Work Bench (twb. rsise. anu. edu. au) without these extensive optimisations. Its one-pass nature also makes it amenable to parallel proof-search on multiple processors.
the Description logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles-that is, transitive roles or their super-roles-in number r...
详细信息
ISBN:
(纸本)9783540755586
the Description logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles-that is, transitive roles or their super-roles-in number restrictions. When modeling composite objects, for example in bio-medical ontologies, this restriction can pose problems.X therefore, we take a closer look at the problem of counting over non-simple roles. On the one hand, we sharpen the known undecidability results and demonstrate that: (i) for DLs with inverse roles, counting over non-simple roles leads to undecidability even when there is only one role in the language;(ii) for DLs without inverses, two transitive and an arbitrary role are sufficient for undecidability. On the other hand, we demonstrate that counting over non-simple roles does not compromise decidability in the absence of inverse roles provided that certain restrictions on role inclusion axioms are satisfied.
We study agents situated in partially observable environments, who do not have the resources to create conformant plans. Instead, they create conditional plans which are partial, and learn from experience to choose th...
详细信息
ISBN:
(纸本)9783540766308
We study agents situated in partially observable environments, who do not have the resources to create conformant plans. Instead, they create conditional plans which are partial, and learn from experience to choose the best of them for execution. Our agent employs an incomplete symbolic deduction system based on Active logic and Situation Calculus for reasoning about actions and their consequences. An Inductive logicprogramming algorithm generalises observations and deduced knowledge in order to choose the best plan for execution. We show results of using PROGOL learning algorithm to distinguish "bad" plans, and we present three modifications which make the algorithm fit this class of problems better. Specifically, we limit the search space by fixing semantics of conditional branches within plans, we guide the search by specifying relative relevance of portions of knowledge base, and we integrate learning algorithm into the agent architecture by allowing it to directly access the agent's knowledge encoded in Active logic. We report on experiments which show that those extensions lead to significantly better learning results.
We extend the Description logic ALC with a "typicality" operator T that allows us to reason about the prototypical properties and inheritance with exceptions. the resulting logic is called ALC + T. the typic...
详细信息
ISBN:
(纸本)9783540755586
We extend the Description logic ALC with a "typicality" operator T that allows us to reason about the prototypical properties and inheritance with exceptions. the resulting logic is called ALC + T. the typicality operator is intended to select the "most normal" or "most typical" instances of a concept. In our framework, knowledge bases may then contain, in addition to ordinary ABoxes and TBoxes, subsumption relations of the form "T(C) is subsumed by P", expressing that typical C-members have the property P. the semantics of a typicality operator is defined by a set of postulates that are strongly related to Kraus-Lehmann-Magidor axioms of preferential logic P. We first show that T enjoys a simple semantics provided by ordinary structures equipped by a preference relation. this allows us to obtain a modal interpretation of the typicality operator. Using such a modal interpretation, we present a tableau calculus for deciding satisfiability of ALC + T knowledge bases. Our calculus gives a nondeterministic-exponential time decision procedure for satisfiability of ALC + T. We then extend ALC + T knowledge bases by a nonmonotonic completion that allows inferring defeasible properties of specific concept instances(1).
the first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded b...
详细信息
ISBN:
(纸本)9783540755586
the first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. the resulting logic, which we call mu MALL(=), satisfies two fundamental proof theoretic properties. In particular mu MALL(=) satisfies cut-elimination, which implies consistency, and has a complete focused proof system. this second result about focused proofs provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We then consider applying these two results about mu MALL(=) to derive a focused proof system for an intuitionistic logic extended with induction and co-induction. the traditional approach to encoding intuitionistic logic into linear logic relies heavily on using the exponentials, which unfortunately weaken the focusing discipline. We get a better focused proof system by observing that certain fixed points satisfy the structural rules of weakening and contraction (without using exponentials). the resulting focused proof system for intuitionistic logic is closely related to the one implemented in Bedwyr, a recent model checker based on logicprogramming. We discuss how our proof theory might be used to build a computational system that can partially automate induction and co-induction.
this paper presents an argument-based logic for reasoning about allocations of the burden of persuasion. the logic extends the system of Prakken (2001), which in turn modified the system of Prakken & Sartor (1996)...
详细信息
ISBN:
(纸本)1595936807
this paper presents an argument-based logic for reasoning about allocations of the burden of persuasion. the logic extends the system of Prakken (2001), which in turn modified the system of Prakken & Sartor (1996) withthe possibility to distribute the burden of proof over both sides in an argument game. First the (2001) system is put in the context of a distinction of three types of proof burdens and it is argued that the proof burdens of that system are in fact burdens of persuasion. then the (2001) system is modified to allow for defeasible reasoning about allocations of such burdens within the logic. the usefulness of the resulting system is illustrated with applications to real legal cases. Copyright 2007 ACM.
In distributed systems, learning does not necessarily involve the participation of agents directly in the inductive process itself. Instead, many systems frequently employ multiple instances of induction separately. I...
详细信息
In distributed systems, learning does not necessarily involve the participation of agents directly in the inductive process itself. Instead, many systems frequently employ multiple instances of induction separately. In this paper, we develop and evaluate a new approach for learning in distributed systems that tightly integrates processes of induction between agents, based on inductive logicprogramming techniques. the paper's main contribution is the integration of an epistemic approach to reasoning about knowledge with inverse entailment during induction. the new approach facilitates a systematic approach to the sharing of knowledge and invention of predicates only when required. We illustrate the approach using the well-known path planning problem and compare results empirically to ( multiple instances of) single agent-based induction over varying distributions of data. Given a chosen path planning algorithm, our algorithm enables agents to combine their local knowledge in an effective way to avoid central control while significantly reducing communication costs.
暂无评论