We present a logic for reasoning about properties of agent programs under different agent execution strategies. Using the agent programming language SimpleAPL as an example, we show how safety and liveness properties ...
详细信息
ISBN:
(纸本)9780981738123
We present a logic for reasoning about properties of agent programs under different agent execution strategies. Using the agent programming language SimpleAPL as an example, we show how safety and liveness properties can be expressed by translating agent programs into expressions of the logic. We give sound and complete axiomatizations of two different program execution strategies for SimpleAPL programs, and, for each of those strategies, prove a correspondence between the operational semantics of SimpleAPL and the models of the corresponding logic.
作者：
Torsten SchaubSchool of Computing Science
Simon Fraser University Burnaby Canada and The Institute for Integrated and Intelligent Systems Griffith University Brisbane Australia and Universität Potsdam Institut für Informatik Potsdam Germany
the field of knowledge representation and reasoning has been going through a methodological shift during recent years. While the past was dominated by query-oriented reasoning, model-based techniques become more and m...
ISBN:
(纸本)9783540789680
the field of knowledge representation and reasoning has been going through a methodological shift during recent years. While the past was dominated by query-oriented reasoning, model-based techniques become more and more popular nowadays. this development was primarily driven by the availability of highly efficient Boolean constraint solvers, like satisfiability and answer set solvers. the general idea is to translate an application problem into a logical specification. this specification is in turn passed to a solver, which outputs models representing solutions to the initial application *** talk will provide an introduction to answer set programming (ASP), its proof-theoretic foundations, methodology, implementation techniques along with a glimpse of an exemplary application. Besides knowledge representation and reasoning, ASP has its roots in deductive databases, nonmonotonicreasoning, and logicprogramming. Applications are specified in ASP in terms of sets of logical rules. Modern ASP solvers rely on high-performance Boolean constraint solving techniques, which allow them to tackle application domains consisting of millions of variables. Meanwhile, this approach proved to be an effective tool in a range of applications, like planning, model checking, and bio-informatics.
the article provides a uniform representation of abductive reasoning in the logical framework of causal inference relations. the representation covers in a single framework not only traditional, classical forms of abd...
详细信息
the article provides a uniform representation of abductive reasoning in the logical framework of causal inference relations. the representation covers in a single framework not only traditional, classical forms of abduction, but also abductive reasoning in diagnosis, theories of actions and change, and abductive logicprogramming.
the article provides a uniform representation of abductive reasoning in the logical framework of causal inference relations. the representation covers in a single framework not only traditional, classical forms of abd...
详细信息
the article provides a uniform representation of abductive reasoning in the logical framework of causal inference relations. the representation covers in a single framework not only traditional, classical forms of abduction, but also abductive reasoning in diagnosis, theories of actions and change, and abductive logicprogramming.
this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and nonmonotonicreasoning. the aims of the c...
详细信息
ISBN:
(纸本)9783540721994
this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and nonmonotonicreasoning. the aims of the competition were twofold: first, to collect challenging benchmark problems, and second, to provide a platform to assess a broad variety of Answer Set programming systems. the competition was inspired by similar events in neighboring fields, where regular benchmarking has been a major factor behind improvements in the developed systems and their ability to address practical applications.
We show how to deploy the CIFF System 4.0 for abductive logicprogramming with constraints in a number of applications, ranging from combinatorial applications to web management. We also compare the CIFF System 4.0 wi...
详细信息
ISBN:
(纸本)9783540721994
We show how to deploy the CIFF System 4.0 for abductive logicprogramming with constraints in a number of applications, ranging from combinatorial applications to web management. We also compare the CIFF System 4.0 with a number of logicprogramming tools, namely the A-System, the DLV system and the SMODELS system.
We describe a new grounder system for logic programs under answer set semantics, called GrinGo. Our approach combines and extends techniques from the two primary grounding approaches of lparse and dlv. A major emphasi...
详细信息
ISBN:
(纸本)9783540721994
We describe a new grounder system for logic programs under answer set semantics, called GrinGo. Our approach combines and extends techniques from the two primary grounding approaches of lparse and dlv. A major emphasis lies on an extensible design that allows for an easy incorporation of new language features in an efficient system environment.
We describe the development of a constraint logicprogramming based system, called CPP, which is capable of generating most preferred plans with respect to a user's preference and evaluate its performance.
ISBN:
(纸本)9783540721994
We describe the development of a constraint logicprogramming based system, called CPP, which is capable of generating most preferred plans with respect to a user's preference and evaluate its performance.
Reiter's default logic formalizes nonmonotonicreasoning using default assumptions. the semantics of a given instance of default logic is based on a fixpoint equation defining an extension. three different reasoni...
详细信息
ISBN:
(纸本)9783540721994
Reiter's default logic formalizes nonmonotonicreasoning using default assumptions. the semantics of a given instance of default logic is based on a fixpoint equation defining an extension. three different reasoning problems arise in the context of default logic, namely the existence of an extension, the presence of a given formula in an extension, and the occurrence of a formula in all extensions. Since the end of 1980s, several complexity results have been published concerning these default reasoning problems for different syntactic classes of formulas. We derive in this paper a complete classification of default logicreasoning problems by means of universal algebra tools using Post's clone lattice. In particular we prove a trichotomy theorem for the existence of an extension, classifying this problem to be either polynomial, NP-complete, or Sigma P-2-complete, depending on the set of underlying Boolean connectives. We also prove similar trichotomy theorems for the two other algorithmic problems in connection with default logicreasoning.
A recently proposed module system for answer set programming is generalized for the input language of the SMODELS system. To show that the stable model semantics is compositional and modular equivalence is a congruenc...
详细信息
ISBN:
(纸本)9783540721994
A recently proposed module system for answer set programming is generalized for the input language of the SMODELS system. To show that the stable model semantics is compositional and modular equivalence is a congruence for composition of SMODELS program modules, a general translation-based scheme for introducing syntactic extensions of the module system is presented. A characterization of the compositionality of the semantics is used as an alternative condition for module composition, which allows compositions of modules even in certain cases with positive recursion between the modules to be composed.
暂无评论