In Answer-Set programming different notions of equivalence, Such as the prominent notions of strong and uniform equivalence, have been studied and characterized by various selections of models in the logic of Here-and...
详细信息
ISBN:
(纸本)9783540899815
In Answer-Set programming different notions of equivalence, Such as the prominent notions of strong and uniform equivalence, have been studied and characterized by various selections of models in the logic of Here-and-there (HT). For uniform equivalence however, Correct characterizations in terms of HT-models can only be obtained for finite theories, respectively programs. In this paper, we show that a selection of countermodels in HT captures uniform equivalence also for infinite theories. this result is turned into coherent characterizations of the different notions of equivalence by countermodels, as well as by a mixture of HT-models and countermodels (so-called equivalence interpretations), which are lifted to first-order theories Under a very general semantics given in terms of a quantified version of HT. We show that countermodels exhibit expedient properties like I simplified treatment of extended signatures, and provide further results for non-ground logic programs. In particular, uniform equivalence coincides under open and ordinary answer-set semantics, and for finite non-ground programs Under these semantics, also the usual characterization of uniform equivalence in terms of maximal and total HT-models of the grounding is correct, even for infinite domains, when corresponding ground programs are infinite.
the system cc inverted perpendicular is a tool for testing correspondence between propositional logic programs under the answer-set semantics with respect to different refined notions of program correspondence. the un...
详细信息
ISBN:
(纸本)9783642006746
the system cc inverted perpendicular is a tool for testing correspondence between propositional logic programs under the answer-set semantics with respect to different refined notions of program correspondence. the underlying methodology of cc inverted perpendicular is to reduce a given correspondence problem to the satisfiability problem of quantified propositional logic and to employ extant solvers for the latter language as back-end inference engines. In a previous version of cc inverted perpendicular, the system was designed to test correspondence between programs based on relativised strong equivalence under answer-set projection. Such a setting generalises the standard notion of strong equivalence by taking the alphabet of the context programs as well as the projection of the compared answer sets to a set of designated output atoms into account. this paper outlines a newly added component of cc inverted perpendicular for testing similarly parameterised correspondence problems based on uniform equivalence.
In this paper we study the problem of concept contraction for the description logic EL. Concept contraction is concerned withthe following question: Given two concepts C and D (withthe interesting case being that D ...
详细信息
ISBN:
(纸本)9780999241172
In this paper we study the problem of concept contraction for the description logic EL. Concept contraction is concerned withthe following question: Given two concepts C and D (withthe interesting case being that D subsumes C) how can we find a generalisation of C that is not subsumed by D but is otherwise as similar as possible to C? We take an AGM-style approach and model this problem using the notion of a concept contraction operator. We consider constructive definitions as well as sets of postulates for concept contraction, and link the two by means of representation theorems.
From point of view of power engineering the successful commercial market with electric vehicles demands a completely new concept of their integration into contemporary electrical network. the electric vehicles have ve...
详细信息
ISBN:
(纸本)9781509009084
From point of view of power engineering the successful commercial market with electric vehicles demands a completely new concept of their integration into contemporary electrical network. the electric vehicles have very limited range, so they have to be charged in short periods, that means for the grid problems with peaks in the daily load profile. the paper outlined one of the most promising - decentralization of the network with help of multiagent systems. Each agent collects and evaluates data about vehicles from small area, manages such area relative independently, so the main problem is to create an algorithm for optimal cooperation and communication withthe other agents. the example of such cooperation is shown, firstly as the simple linear programming problem, the secondly more complex, with using the game theory which is the mathematical basis for multiagent systems. the system is connected withthe smart grid, so the possibilities of altering the load profile are shown. the last chapter explores the necessity of the shift of such grid to artificial intelligence and the epistemic modal logic is presented as a possible solution.
Standard game theory models implicitly assume that all significant aspects of a game (payoffs, moves available, etc.) are common knowledge among the players. there are well-known techniques going back to Harsanyi [4] ...
详细信息
this paper presents a solution based on subjective logic to include 'second-order uncertainty' in objective functions for mission-driven resource allocation. When resources have to be optimized, one of the req...
详细信息
ISBN:
(纸本)9781479916344
this paper presents a solution based on subjective logic to include 'second-order uncertainty' in objective functions for mission-driven resource allocation. When resources have to be optimized, one of the requirements is a probabilistic assessment of future scenarios. However, the end-users who have to convey such future assessment may not be completely confident about it. It can therefore be necessary to specify a confidence level together withthis input. With subjective logic it is possible to describe such second-order uncertainty. We used it to describe the uncertainty of assessments (e.g. about future threats) and models (e.g. of sensor systems) within the optimization objective. As a result, the integrity of the optimization improves, because excluding important uncertainties from the optimality definition is not, actually, optimal. In the end, although it is complicated to incorporate different levels of uncertainty, the resulting analysis about mission outcomes is more genuine, it creates transparency towards the end-users, and eventually, results in a resource allocation solution that takes more aspects into account.
In this paper, we present a goal-directed proof procedure for ASP with abduction. Our proposed procedure in this paper is correct for any consistent abductive framework proposed in [Kakas90a]. In other words, if the p...
详细信息
Nondeterministic strategies are strategies (or protocols, or plans) that, given a history in a game, assign a set of possible actions, all of which should be winning. An important problem is that of refining such stra...
详细信息
ISBN:
(纸本)9780999241172
Nondeterministic strategies are strategies (or protocols, or plans) that, given a history in a game, assign a set of possible actions, all of which should be winning. An important problem is that of refining such strategies. For instance, given a nondeterministic strategy that allows only safe executions, refine it to, additionally, eventually reach a desired state of affairs. We show that strategic problems involving strategy refinement can be solved elegantly in the framework of Strategy logic (SL), a very expressive logic to reason about strategic abilities. Specifically, we introduce an extension of SL with nondeterministic strategies and an operator expressing strategy refinement. We show that model checking this logic can be done at no additional computational cost with respect to standard SL, and can be used to solve a variety of problems such as synthesis of maximally permissive strategies or maximally permissive Nash equilibria.
the logic of information flows (LIF) is a general framework in which tasks of a procedural nature can be modeled in a declarative, logic-based fashion. the first contribution of this paper is to propose semantic and s...
详细信息
ISBN:
(纸本)9780999241172
the logic of information flows (LIF) is a general framework in which tasks of a procedural nature can be modeled in a declarative, logic-based fashion. the first contribution of this paper is to propose semantic and syntactic definitions of inputs and outputs of LIF expressions. We study how the two relate and show that our syntactic definition is optimal in a sense that is made precise. the second contribution is a systematic study of the expressive power of sequential composition in LIF. Our results on composition tie in the results on inputs and outputs, and relate LIF to first-order logic (FO) and bounded-variable LIF to bounded-variable FO.
We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully mac...
详细信息
ISBN:
(纸本)9781450310543
We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked static analyses equipped with efficient theorem provers are now within the reach of formal methods. As a pair, VeriStar and VeriSmall represent the first application of the Verified Software Toolchain [4], a tightly integrated collection of machine-verified program logics and compilers giving foundational correctness guarantees. VeriStar is (1) purely functional, (2) machine-checked, (3) end-to-end, (4) efficient and (5) modular. By purely functional, we mean it is implemented in Gallina, the pure functional programming language embedded in the Coq theorem prover. By machine-checked, we mean it has a proof in Coq that when the prover says "valid", the checked entailment holds in a proved-sound separation logic for C minor. By end-to-end, we mean that when the static analysis+theorem prover says a C minor program is safe, the program will be compiled to a semantically equivalent assembly program that runs on real hardware. By efficient, we mean that the prover implements a state-of-the-art algorithm for deciding heap entailments and uses highly tuned verified functional data structures. By modular, we mean that VeriStar can be retrofitted to other static analyses as a plug-compatible entailment checker and its soundness proof can easily be ported to other separation logics.
暂无评论