We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. this measure, called entanglement, is defined by way of a game that is som...
详细信息
ISBN:
(纸本)3540252363
We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. this measure, called entanglement, is defined by way of a game that is somewhat similar in spirit to the robber and cops games used to describe tree width, directed tree width, and hypertree width. Nevertheless, on many classes of graphs, there are significant differences between entanglement and the various incarnations of tree width. Entanglement is intimately connected to the computational and descriptive complexity of the modal μ-calculus. On the one hand, the number of fixed point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. this plays a crucial role in the proof that the variable hierarchy of the μ-calculus is strict. In addition to this, we prove that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of a subgame induced by a winning strategy.
the paper introduces Answer Set programming with External Predicates (ASP-EX), a framework aimed at enabling ASP to deal with external sources of computation. this feature is realized by the introduction of "para...
详细信息
ISBN:
(纸本)3540285385
the paper introduces Answer Set programming with External Predicates (ASP-EX), a framework aimed at enabling ASP to deal with external sources of computation. this feature is realized by the introduction of "parametric" external predicates, whose extension is not specified by means of a logic program but computed through external code. With respect to existing approaches it is explicitly addressed the issue of invention of new information coming from external predicates, in form of new, and possibly infinite, constant symbols. Several decidable restrictions of the language are identified as well as suitable algorithms for evaluating Answer Set Programs with external predicates. the framework paves the way to Answer Set programming in several directions such as pattern manipulation applications, as well as the possibility to exploit function symbols. ASP-EX has been successfully implemented in the DLV system, which is now enabled to make external program calls.
the extended answer set semantics for simple logic programs, i.e. programs with only classical negation, allows for the defeat of rules to resolve contradictions. In addition, a partial order relation on the program&#...
详细信息
ISBN:
(纸本)3540252363
the extended answer set semantics for simple logic programs, i.e. programs with only classical negation, allows for the defeat of rules to resolve contradictions. In addition, a partial order relation on the program's rules can be used to deduce a preference relation on its extended answer sets. In this paper, we propose a "quantitative" preference relation that associates a weight with each rule in a program. Intuitively, these weights define the "cost" of defeating a rule. An extended answer set is preferred if it minimizes the sum of the weights of its defeated rules. We characterize the expressiveness of the resulting semantics and show that it can capture negation as failure. Moreover the semantics can be conveniently extended to sequences of weight preferences, without increasing the expressiveness. We illustrate an application of the approach by showing how it can elegantly express subgraph isomorphic approximation problems, a concept often used in intelligence analysis to find specific regions of interest in a large graph of observed activities.
Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed point logic (FPL) extension of C...
详细信息
ISBN:
(纸本)3540285385
Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed point logic (FPL) extension of Clark's completion such that open answer sets correspond to models of FPL formulas and identify a syntactic subclass of programs, called (loosely) guarded programs. Whereas reasoning with general programs in OASP is undecidable, the FPL translation of (loosely) guarded programs falls in the decidable (loosely) guarded fixed point logic (mu(L)GF). Moreover, we reduce normal closed ASP to loosely guarded OASP, enabling a characterization of an answer set semantics by mu LGF formulas. Finally, we relate guarded OASP to Datalog LITE, thus linking an answer set semantics to a semantics based on fixed point models of extended stratified Datalog programs. From this correspondence, we deduce 2-EXPTIME-completeness of satisfiability checking w.r.t. (loosely) guarded programs.
the Tag-Frame system of resource management [1] reunited two divergent threads of linear logicprogramming research by achieving the efficient proof search behaviour of abstract systems, such as [2), while using a low...
详细信息
ISBN:
(纸本)3540252363
the Tag-Frame system of resource management [1] reunited two divergent threads of linear logicprogramming research by achieving the efficient proof search behaviour of abstract systems, such as [2), while using a low-level tag-based approach, as in [31, suitable for specifying an abstract machine. However, Tag-Frame relies on set operations which are linear in the size of the sets, and is not as efficient, in general, as it could be. We present a new tag-based derivation system which relies solely on low-level concepts to implement efficient resource management, where most linear time operations have been replaced by constant time ones. though motivated and informed by the Tag-Frame system, we derive our system directly from, and prove its correctness with respect to the system of Cervesato et al. [2]. An abstract machine based on the new system has been implemented by Tamura and Banbara, and its performance compared to their previous machine.
the formalism of nonmonotonic causal theories (Ciunchiglia, Lee, Lifschitz, McCain, Turner, 2004) provides a general-purpose formalism for nonmonotonic reasoning and knowledge representation, as well as a higher level...
详细信息
ISBN:
(纸本)3540285385
the formalism of nonmonotonic causal theories (Ciunchiglia, Lee, Lifschitz, McCain, Turner, 2004) provides a general-purpose formalism for nonmonotonic reasoning and knowledge representation, as well as a higher level, special-purpose notation, the action language C+, for specifying and reasoning about the effects of actions and the persistence ('inertia') of facts over time. In this paper we investigate some logical properties of these formalisms. there are two motivations. From the technical point of view, we seek to gain additional insights into the properties of the languages when viewed as a species of conditional logic. From the practical point of view, we are seeking to find conditions under which two different causal theories, or two different action descriptions in C+, can be said to be equivalent, withthe further aim of helping to decide between alternative formulations when constructing practical applications.
We introduce Abstract DPLL, a general and simple abstract rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Its properties, such as soundness, completeness or termination, immediately carr...
详细信息
ISBN:
(纸本)3540252363
We introduce Abstract DPLL, a general and simple abstract rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as non-chronological backtracking or clause learning. this allows one to formally reason about practical DPLL algorithms in a simple way. In the second part of this paper we extend the framework to Abstract DPLL modulo theories. this allows us to express-and formally reason about-state-of-the-art concrete DPLL-based techniques for satisfiability modulo background theories, such as the different lazy approaches, or our DPLL(T) framework.
the inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. the logic of Bunched Implications (BI), due to Pyrn and O'Hearn, is a log...
详细信息
ISBN:
(纸本)3540252363
the inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. the logic of Bunched Implications (BI), due to Pyrn and O'Hearn, is a logic which freely combines the familiar connectives of intuitionistic logic with multiplicative linear conjunction and its adjoint implication. We present the first formulation of an inverse method for propositional BI without units. We adapt the sequent calculus for BI into a forward calculus. the soundness and completeness of the calculus are proved, and a canonical form for bunches is given.
the coupling of description logicreasoning systems with other reasoning formalisms (possibly over the Web) is becoming an important research issue and calls for advanced methods and algorithms. Recently, several noti...
详细信息
ISBN:
(纸本)3540252363
the coupling of description logicreasoning systems with other reasoning formalisms (possibly over the Web) is becoming an important research issue and calls for advanced methods and algorithms. Recently, several notions of description logic programs have been introduced, combining rule-based semantics with description logics. Among them are nonmonotonic description logic programs (or dl-programs for short) which combine nonmonotonic logic programs with description logics under a generalized version of the answer-set and the well-founded semantics, respectively, which are the predominant semantics for nonmonotonic logic programs. In this paper, we consider some technical issues regarding an efficient implementation for both semantics, which has been realized in a working prototype exploiting the two state-of-art tools DLV and RACER. A major issue in this respect is efficient interfacing between the two reasoning systems at hand, for which we devised special methods. Such methods may fruitfully be used for the implementation of systems of similar nature. Reported experimentation activities with our prototype show that the methods we have developed are effective and are a key for highly optimized nonmonotonic dl-program engines.
the dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible methods to prove termination. In this...
详细信息
ISBN:
(纸本)3540252363
the dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible methods to prove termination. In this paper, we show that dependency pairs can instead be used as a general concept to integrate arbitrary techniques for termination analysis. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. We refer to this new concept as the "dependency pair framework" to distinguish it from the old "dependency pair approach". Moreover, this framework facilitates the development of new methods for termination analysis. To demonstrate this, we present several new techniques within the dependency pair framework which simplify termination problems considerably. We implemented the dependency pair framework in our termination prover AProVE and evaluated it on large collections of examples.
暂无评论