Tableau calculi are the state-of-the-art for reasoning in description logics (DL). Despite recent improvements, tableau-based reasoners still cannot process certain knowledge bases (KBs), mainly because they end Lip b...
详细信息
ISBN:
(纸本)9783540710691
Tableau calculi are the state-of-the-art for reasoning in description logics (DL). Despite recent improvements, tableau-based reasoners still cannot process certain knowledge bases (KBs), mainly because they end Lip building very large models. To address this, we propose a tableau calculus with individual reuse: to satisfy an existential assertion, our calculus nondeterministically tries to reuse individuals from the model generated thus far. We present two expansion strategies: one is applicable to the DL ELOH and gives us a worst-case optimal algorithm, and the other is applicable to the DL SHOIQ, Using this technique, our reasoner can process several KBs that no other reasoner can.
the proceedings contain 43 papers. the topics discussed include: on a hybrid symbolic-connectionist approach for modeling the kinematic robot map - and benchmarks for computer algebra;applying link grammar formalism i...
详细信息
ISBN:
(纸本)3540851097
the proceedings contain 43 papers. the topics discussed include: on a hybrid symbolic-connectionist approach for modeling the kinematic robot map - and benchmarks for computer algebra;applying link grammar formalism in the development of English-Indonesian machine translation system;case studies in model manipulation for scientific computing;mechanising a proof of Craig's interpolation theorem for intuitionistic logic in nominal Isabelle;ASIC meets natural typography;the monoids of order eight and nine;extending graphical representations for compact closed categories with applications to symbolic quantum computation;a full first-order constraint solver for decomposable theories;search techniques for rational polynomial orders;strategies for solving sat in grids by randomized search;towards an implementation of a computer algebra system in a functional language;and automated model building: from finite to infinite models.
State-of-the-art implementations of common aspect-oriented languages weave residual dispatching logic for advice whose applicability cannot be determined at compile-time. But being derived from the residue's formu...
详细信息
ISBN:
(纸本)9781605581101
State-of-the-art implementations of common aspect-oriented languages weave residual dispatching logic for advice whose applicability cannot be determined at compile-time. But being derived from the residue's formula representation the woven code often implements an evaluation strategy which mandates redundant evaluations of atomic pointcuts. In order to improve upon the average-case run-time cost, this paper presents an alternative representation which enables efficient residual dispatch, namely ordered binary decision diagrams. In particular, this representation facilitates the complete elimination of redundant evaluations across all point-cuts sharing a join point shadow. Copyright 2008 ACM.
We propose a formal model to represent and solve the Constraint-Based Routing problem in networks. To attain this, we model the network adapting it to a weighted or graph (unicast delivery) or and-or graph (multicast ...
详细信息
ISBN:
(纸本)9781424442348
We propose a formal model to represent and solve the Constraint-Based Routing problem in networks. To attain this, we model the network adapting it to a weighted or graph (unicast delivery) or and-or graph (multicast delivery), where the weight on a connector corresponds to the cost of sending a packet on the network link modelled by that connector. We use the Soft Constraint logicprogramming (SCLP) framework as a convenient declarative programming environment in which to solve the routing problem. In particular, we show how the semantics of an SCLP program computes the best route in the corresponding graph. At last, we provide an implementation of the framework over scale free networks.
We introduce a DPLL calculus that is a decision procedure for the Bernays-Schonfinkel class, also known as EPR. Our calculus allows combining techniques for efficient propositional search with data-structures, such as...
详细信息
ISBN:
(纸本)9783540710691
We introduce a DPLL calculus that is a decision procedure for the Bernays-Schonfinkel class, also known as EPR. Our calculus allows combining techniques for efficient propositional search with data-structures, such as Binary Decision Diagrams, that can efficiently and succinctly encode finite sets of substitutions and operations on these. In the calculus, clauses comprise of a sequence of literals together with a finite set of substitutions;truth assignments are also represented using substitution sets. the calculus works directly at the level of sets, and admits performing simultaneous constraint propagation and decisions, resulting in potentially exponential speedups over existing approaches.
We present an integer programming approach to the university course timetabling problem, in which weekly lectures have to be scheduled and assigned to rooms. Students’ curricula impose restrictions as to which course...
详细信息
We investigate the computational complexity of spatial logics extended withthe means to represent topological connectedness and restrict the number of connected components. In particular, we show that the connectedne...
详细信息
ISBN:
(纸本)9783540894384
We investigate the computational complexity of spatial logics extended withthe means to represent topological connectedness and restrict the number of connected components. In particular, we show that the connectedness constraints can increase complexity from NP to PSPACE, EXPTIME and, if component counting is allowed, to NEXPTIME.
the Traveling Tournament Problem with Predefined Venues (TTPPV) is a single round robin variant of the Traveling Tournament Problem, in which the venue of each game to be played is known beforehand. We propose an Iter...
详细信息
the proceedings contain 62 papers. the topics discussed include: supporting collaborative ontology development in Protege;identifying potentially important concepts and relations in an ontology;an experimental compari...
ISBN:
(纸本)3540885633
the proceedings contain 62 papers. the topics discussed include: supporting collaborative ontology development in Protege;identifying potentially important concepts and relations in an ontology;an experimental comparison of RDF data management approaches in a SPARQL benchmark scenario;anytime query answering in RDF through evolutionary algorithms;extracting semantic constraint from description text for Semantic Web service discovery;enhancing semantic Web services with inheritance;using semantic distances for reasoning with inconsistent ontologies;statistical learning for inductive query answering on OWL ontologies;optimization and evaluation of reasoning in probabilistic description logic: towards a systematic approach;and comparison between ontology distances.
For a number of programming languages, among them Eiffel, C, Java and Ruby, Hoare-style logics and dynamic logics have been developed. In these logics, pre- and postconditions are typically formulated using potentiall...
详细信息
ISBN:
(纸本)9783540787426
For a number of programming languages, among them Eiffel, C, Java and Ruby, Hoare-style logics and dynamic logics have been developed. In these logics, pre- and postconditions are typically formulated using potentially effectful programs. In order to ensure that these pre- and postconditions behave like logical formulae (that is, enjoy some kind of referential transparency), a notion of purity is needed. Here, we introduce a generic framework for reasoning about purity and effects. Effects are modeled abstractly and axiomatically, using Moggi's idea of encapsulation of effects as monads. We introduce a dynamic logic (from which, as usual, a Hoare logic can be derived) whose logical formulae are pure programs in a strong sense. We formulate a set of proof rules for this logic, and prove it to be complete with respect to a categorical semantics. Using dynamic logic, we then develop a relaxed notion of purity which allows for observationally neutral effects such writing on newly allocated memory.
暂无评论