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.
Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly ...
详细信息
ISBN:
(纸本)3540252363
Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly optimized for theorem proving with equality. However, even such an advanced calculus does not restrict inferences enough to obtain decision procedures for complex logics, such as SHIQ. In this paper, we present a new decomposition inference rule, which can be combined with any resolution-based calculus compatible withthe standard notion of redundancy. We combine decomposition with basic superposition to obtain three new decision procedures: (i) for the description logic SHIQ, (ii) for the description logic ALCHIQb, and (iii) for answering conjunctive queries over SHIQ knowledge bases. the first two procedures are worst-case optimal and, based on the vast experience in building efficient theorem provers, we expect them to be suitable for practical usage.
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.
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logicprogramming and...
详细信息
ISBN:
(纸本)3540255966
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logicprogramming and term rewriting techniques that provide similar advantages to, but remain simpler than, higher-order logicprogramming or term rewriting systems. Previous work on nominal rewriting and logicprogramming has relied on nominal unification, that is, unification up to equality in nominal logic. However, because of nominal logic's equivariance property, these applications require a stronger form of unification, which we call equivariant unification. Unfortunately, equivariant unification and matching are NP-hard decision problems. this paper presents an algorithm for equivariant unification that produces a complete set of finitely many solutions, as well as NP decision procedure and a version that enumerates solutions one at a time. In addition, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.
Cut-elimination is the most prominent form of proof transformation in logic. the elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. the cut-elim...
详细信息
ISBN:
(纸本)3540252363
Cut-elimination is the most prominent form of proof transformation in logic. the elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. the cut-elimination method CERES (cut-elimination by resolution) works by constructing a set of clauses from a proof with cuts. Any resolution refutation of this set can then serve as a skeleton of a proof with only atomic cuts. In this paper we present a systematic experiment withthe implementation of CERES on a proof of reasonable size and complexity. It turns out that the proof with cuts can be transformed into two mathematically different proofs of the theorem. In particular, the application of positive and negative hyperresolution yield different mathematical arguments. As an unexpected side-effect the derived clauses of the resolution refutation proved particularly interesting as they can be considered as meaningful universal lemmas. though the proof under investigation is intuitively simple, the experiment demonstrates that new (and relevant) mathematical information on proofs can be obtained by computational methods. It can be considered as a first step in the development of an experimental culture of computer-aided proof analysis in mathematics.
In 1969, Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. We know the answer to this question for various subsystems...
详细信息
We give a logicprogramming based account of probability and describe a declarative language P-log capable of reasoning which combines bothlogical and probabilistic arguments. Several non-trivial examples illustrate ...
详细信息
ISBN:
(纸本)354020721X
We give a logicprogramming based account of probability and describe a declarative language P-log capable of reasoning which combines bothlogical and probabilistic arguments. Several non-trivial examples illustrate the use of P-log for knowledge representation.
In this paper, we address the problem of checking whether two disjunctive logic programs possess exactly the same stable models. An existing translation-based method [14], which was designed for weight constraint prog...
详细信息
ISBN:
(纸本)354020721X
In this paper, we address the problem of checking whether two disjunctive logic programs possess exactly the same stable models. An existing translation-based method [14], which was designed for weight constraint programs supported by the SMODELS system, is generalized to the disjunctive case. Moreover, we report on our preliminary experiments with an implementation of the method, a translator called DLPEQ.
nlp is a compiler for nested logicprogramming under answer set semantics. It is designed as a front-end translating nested logic programs into disjunctive ones, whose answer sets are then computable by disjunctive lo...
详细信息
ISBN:
(纸本)354020721X
nlp is a compiler for nested logicprogramming under answer set semantics. It is designed as a front-end translating nested logic programs into disjunctive ones, whose answer sets are then computable by disjunctive logicprogramming systems, like dlv or gnt. nlp offers different translations: One is polynomial but necessitates the introduction of new atoms, another is exponential in the worst case but avoids extending the language. We report experimental results, comparing the translations on several classes of benchmark problems.
LPEQ and DLPEQ, two translators for automated equivalence testing of logic programs are discussed. the translators LPEQ and DLPEQ have been implemented in the C programming language under the Linux operating system. B...
详细信息
ISBN:
(纸本)354020721X
LPEQ and DLPEQ, two translators for automated equivalence testing of logic programs are discussed. the translators LPEQ and DLPEQ have been implemented in the C programming language under the Linux operating system. Both translators take two logic programs and command line options as their input and produce a translation for equivalence testing as their output. the input files are assumed to be in an internal format, as produced by the front-end LPARSE of the SMODELS system.
暂无评论