In this paper a, proof technique for reasoning about the multimodal logic of beliefs and goals is defined based on resolution at different levels of a. tree of clauses. We have considered belief and goal as normal mod...
详细信息
ISBN:
(纸本)3540252363
In this paper a, proof technique for reasoning about the multimodal logic of beliefs and goals is defined based on resolution at different levels of a. tree of clauses. We have considered belief and goal as normal modal logic operators. the technique is inspired by that in [6,7] and allows for a locality property to be satisfied. the main motivation for this work arises not as much from theorem-proving as from the notion of belief and goal revision under an assumption of consistency of the beliefs and goals of an agent. We, also present proofs of soundness and completeness of the logic.
We present the action language GC+ for reasoning about actions in multi-agent systems under probabilistic uncertainty and partial observability, which is an extension of the action language C+ that is inspired by part...
详细信息
ISBN:
(纸本)3540285385
We present the action language GC+ for reasoning about actions in multi-agent systems under probabilistic uncertainty and partial observability, which is an extension of the action language C+ that is inspired by partially observable stochastic games (POSGs). We provide a finite-horizon value iteration for this framework and show that it characterizes finite-horizon Nash equilibria. We also describe how the framework can be implemented on top of nonmonotonic causal theories. We then present acyclic action descriptions in GC+ as a special case where transitions are computable in polynomial time. We also give an example that shows the usefulness of our approach in practice.
Nested logic programs and epistemic logic programs are two important extensions of answer set programming. However, the relationship between these two formalisms is rarely explored. In this paper we first introduce th...
详细信息
ISBN:
(纸本)3540285385
Nested logic programs and epistemic logic programs are two important extensions of answer set programming. However, the relationship between these two formalisms is rarely explored. In this paper we first introduce the epistemic HT-logic, and then propose a more general extension of logic programs called nested epistemic logic programs. the semantics of this extension - named equilibrium views - is defined on the basis of the epistemic HT-logic. We prove that equilibrium view semantics extends boththe answer sets of nested logic programs and the world views of epistemic logic programs. therefore, our work establishes a unifying framework for both nested logic programs and epistemic logic programs. Furthermore, we also provide a characterization of the strong equivalence of two nested epistemic logic programs.
We investigate techniques for approximating answer sets of general logic programs of Lifschitz and Woo, whose rules have single literals as heads. We propose three different methods of approximation and obtain results...
详细信息
ISBN:
(纸本)3540285385
We investigate techniques for approximating answer sets of general logic programs of Lifschitz and Woo, whose rules have single literals as heads. We propose three different methods of approximation and obtain results on the relationship between them. Since general logic programs with single literals as heads are equivalent to revision programs, we obtain results on approximations of justified revisions of databases by revision programs.
We consider the problem of identifying equivalence of two knowledge bases which are capable of abductive reasoning. Here, a knowledge base is written in either first-order logic or nonmonotonic logicprogramming. In t...
详细信息
We consider the problem of identifying equivalence of two knowledge bases which are capable of abductive reasoning. Here, a knowledge base is written in either first-order logic or nonmonotonic logicprogramming. In this work, we will give two definitions of abductive equivalence. the first one, explainable equivalence, requires that two abductive programs have the same explainability for any observation. Another one, explanatory equivalence, guarantees that any observation has exactly the same explanations in each abductive framework. Explanatory equivalence is a stronger notion than explainable equivalence. In first-order abduction, explainable equivalence can be verified by the notion of extensional equivalence in default theories. In nonmonotonic logic programs, explanatory equivalence can be checked by means of the notion of relative strong equivalence. We also show the complexity results for abductive equivalence.
the proceedings contain 26 papers from the conference on Inductive logicprogramming15thinternationalconference, ILP 2005. the topics discussed include: guiding inference through relational reinforcement learning;c...
详细信息
the proceedings contain 26 papers from the conference on Inductive logicprogramming15thinternationalconference, ILP 2005. the topics discussed include: guiding inference through relational reinforcement learning;converting semantic meta-knowledge into inductive bias;distance based generaliztion;automatic induction of abduction and abstraction theories from observations;strategies to parallelize ILP systems;inducing casual laws by regular inferece;spatial clustering of structured objects;predicate selection for structural decision trees;inductive equivalence of logic programs;and a study of applying dimensionality reduction to restrict the size of a hypothesis space.
Separation logic is a subset of the quantifier-free first order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipe...
详细信息
ISBN:
(纸本)354030553X
Separation logic is a subset of the quantifier-free first order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipelined processor designs and timed systems, In this paper, we present a fast decision procedure for separation logic, which combines Boolean satisfiability (SAT) with a graph based incremental negative cycle elimination algorithm. Our solver abstracts a separation logic formula into a Boolean formula by replacing each predicate with a Boolean variable. Transitivity constraints over predicates are detected from the constraint graph and added on a need-to basis. Our solver handles Boolean and theory conflicts uniformly at the Boolean level. the graph based algorithm supports not only incremental theory propagation, but also constant time theory backtracking without using a cumbersome history stack. Experimental results on a large set of benchmarks show that our new decision procedure is scalable, and outperforms existing techniques for this logic.
In this paper, we focus on the problem of learning reactive skills for use by physical agents. We propose a new representation for such procedures, teleoreactive logic programs, along with an interpreter that utilizes...
详细信息
ISBN:
(纸本)3540281770
In this paper, we focus on the problem of learning reactive skills for use by physical agents. We propose a new representation for such procedures, teleoreactive logic programs, along with an interpreter that utilizes them to achieve goals. After this, we describe a learning method that acquires these structures in a cumulative manner through problem solving. We report experiments in three domains that involve multiple levels of skilled behavior. We also review related work and discuss directions for future research.
We describe Modular-E (ME), a specialized, modeltheoretic logic for narrative reasoning about actions, able to represent non-deterministic domains involving concurrency, static laws (constraints) and indirect effects ...
详细信息
ISBN:
(纸本)3540285385
We describe Modular-E (ME), a specialized, modeltheoretic logic for narrative reasoning about actions, able to represent non-deterministic domains involving concurrency, static laws (constraints) and indirect effects (ramifications). We give formal results which characterize ME's high degree of modularity and elaboration tolerance, and show how these properties help to separate out, and provide a principled solutions to, the endogenous and exogenous qualification problems. We also show how a notion of (micro) processes can be used to facilitate reasoning at the dual levels of temporal granularity necessary for narrative-based domains involving "instantaneous" series of indirect and knock-on effects.
Equilibrium logic, introduced by David Pearce, extends the concept of an answer set from logic programs to arbitrary sets of formulas. logic programs correspond to the special case in which every formula is a "ru...
详细信息
ISBN:
(纸本)3540285385
Equilibrium logic, introduced by David Pearce, extends the concept of an answer set from logic programs to arbitrary sets of formulas. logic programs correspond to the special case in which every formula is a "rule" - an implication that has no implications in the antecedent (body) and consequent (head). the semantics of equilibrium logic looks very different from the usual definitions of an answer set in logicprogramming, as it is based on Kripke models. In this paper we propose a new definition of equilibrium logic which uses the concept of a reduct, as in the standard definition of an answer set. Second, we apply the generalized concept of an answer set to the problem of defining the semantics of aggregates in answer set programming. We propose, in particular, a semantics for weight constraints that covers the problematic case of negative weights. Our semantics of aggregates is an extension of the approach due to Faber, Leone, and Pfeifer to a language with choice rules and, more generally, arbitrary rules with nested expressions.
暂无评论