We describe an application of Abductive logicprogramming (ALP) to the analysis of an important class of DNA microarray experiments. We develop an ALP theory that provides a simple and general model of how gene intera...
详细信息
ISBN:
(纸本)3540285385
We describe an application of Abductive logicprogramming (ALP) to the analysis of an important class of DNA microarray experiments. We develop an ALP theory that provides a simple and general model of how gene interactions can cause changes in observable expression levels of genes. Input to the procedure are the observed microarray results;output are hypotheses about possible gene interactions that explain the observed effects. We apply and evaluate our approach on microarray experiments on M. tuberculosis and S. cerevisiae.
CERES is a method for cut-elimination in classical logic which is based on resolution. In this paper we extend CERES to CERES-m, a resolution-based method of cut-elimination in Gentzen calculi for arbitrary finitely-v...
详细信息
ISBN:
(纸本)3540252363
CERES is a method for cut-elimination in classical logic which is based on resolution. In this paper we extend CERES to CERES-m, a resolution-based method of cut-elimination in Gentzen calculi for arbitrary finitely-valued logics. Like in the classical case the core of the method is the construction of a resolution proof in finitely-valued logics. Compared to Gentzen-type cut-elimination methods the advantage of CERES-m is a twofold one: 1. it is easier to define and 2. it is computationally superior and thus more appropriate for implementations and experiments.
We present efficient Pure Pointer Machine (PPM) algorithms to test for "leftness" in dynamic search trees and related problems. In particular, we show that the problem of testing if a node x is in the leftmo...
详细信息
ISBN:
(纸本)354030553X
We present efficient Pure Pointer Machine (PPM) algorithms to test for "leftness" in dynamic search trees and related problems. In particular, we show that the problem of testing if a node x is in the leftmost branch of the subtree rooted in node y, in a dynamic tree that grows and shrinks at the leaves, can be solved on PPMs in worst-case O((lg lg n)(2)) time per operation in the semi-dynamic case-i.e., all the operations that add leaves to the tree are performed before any other operations-where n is the number of operations that affect the structure of the tree. We also show that the problem can be solved on PPMs in amortized O((lg lg n)(2)) time per operation in the fully dynamic case.
We observe, that subsumption of clauses (in the language of first order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption take...
详细信息
ISBN:
(纸本)3540252363
We observe, that subsumption of clauses (in the language of first order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption takes roughly half of the running time of a typical first order resolution-based theorem prover. We also give some experimental evidence, that replacing syntactic indexing for subsumption by our semantic Monte Carlo technique can, in some situations, significantly decrease the cost of subsumption. testing. Finally, we provide some evidence that a similar semantic idea can be probably successfully used for testing for AC matching, which is another NP-complete problem whose millions of instances are being solved by theorem provers.
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.
Revising and updating knowledge bases is an important issue in knowledge representation and reasoning. Various proposals have been made recently for updating logic programs, in particular with respect to answer set pr...
详细信息
Revising and updating knowledge bases is an important issue in knowledge representation and reasoning. Various proposals have been made recently for updating logic programs, in particular with respect to answer set programming. So far, most of these approaches are based on the causal rejection principle but most of them are showing an unintuitive behaviour. Our update semantics (based on minimal generalised answer sets) satisfies several structural properties and avoids problems of the other proposals. In additionwe introduce some new properties that we consider an updating/dynamic semantics should fulfill too: Weak Irrelevance of Syntax and Strong Consistency. We compare our approach withthe well-known upd operator due to Eiter et al. and show that it satisfies the new properties.
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.
the notion of comparative similarity 'X is more similar or closer to Y than to Z' has been investigated in both foundational and applied areas of knowledge representation and reasoning, e.g., in concept format...
详细信息
ISBN:
(纸本)354030553X
the notion of comparative similarity 'X is more similar or closer to Y than to Z' has been investigated in both foundational and applied areas of knowledge representation and reasoning, e.g., in concept formation, similarity- based reasoning and areas of bioinformatics such as protein sequence alignment. In this paper we analyse the computational behaviour of the 'propositional' logic withthe binary operator 'closer to a set tau(1) than to a set tau(2)' and nominals interpreted over various classes of distance (or similarity) spaces. In particular, using a reduction to the emptiness problem for certain tree automata, we show that the satisfiability problem for this logic is ExpTime- complete for the classes of all finite symmetric and all finite (possibly non-symmetric) distance spaces. For finite subspaces of the real line (and higher dimensional Euclidean spaces) we prove the undecidability of satisfiability by a reduction of the solvability problem for Diophantine equations. As our closer' operator has the same expressive power as the standard operator > of conditional logic, these results may have interesting implications for conditional logic as well.
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.
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.
暂无评论