This paper is concerned with the design of type systems for logicprogramming so as to satisfy the requirements of modern logicprogramming. The design of type systems is based on the language Godel which has a strong...
详细信息
ISBN:
(纸本)9781424421961
This paper is concerned with the design of type systems for logicprogramming so as to satisfy the requirements of modern logicprogramming. The design of type systems is based on the language Godel which has a strongly type system based on many-sorted logic with parametric polymorphism. The definitions of the basic logicprogramming concepts of terms, atoms, programs are given in the setting of polymorphic many-sorted logic. In particular, an unification algorithm for typed predicates is proposed for the compiler construction of Godel.
We focus on families of Pawlak approximation spaces, called multiple-source approximation systems (MSASs). These reflect the situation where information arrives from multiple sources. The behaviour of rough sets in MS...
详细信息
We focus on families of Pawlak approximation spaces, called multiple-source approximation systems (MSASs). These reflect the situation where information arrives from multiple sources. The behaviour of rough sets in MSASs is investigated - different notions of lower and upper approximations, and definability of a set in a MSAS are introduced. In this context, a generalized version of an information system, viz. multiple-source knowledgerepresentation (KR)-system, is discussed. Apart from the indiscernibility relation which can be defined on a multiple-source KR-system, two other relations, viz. similarity and inclusion are considered. To facilitate formal reasoning with rough sets in MSASs, a quantified propositional modal logic LMSAS is proposed. Interpretations for sets of well-formed formulae (wffs) of LMSAS are defined on MSASs, and the various properties of rough sets in MSASs translate into logically valid wffs of the system. LMSAS is shown to be sound and complete with respect to this semantics. Some decidable problems are addressed. In particular, it is shown that for any LMSAS-wff alpha it is possible to check whether alpha is satisfiable in a certain class of interpretations with MSASs of a given finite cardinality. Moreover, it is also decidable whether any wff alpha is satisfiable in the class of all interpretations with MSASs having domain of a given finite cardinality. (C) 2008 Elsevier Inc. All rights reserved.
An ultra-low power logic NVM has currents <10nA/cell in all operating regimes, high programming/erase speeds, excellent endurance/retention and allows strong Vdd fluctuations. The memory uses CMOS inverter read-out...
详细信息
ISBN:
(纸本)9781424415465
An ultra-low power logic NVM has currents <10nA/cell in all operating regimes, high programming/erase speeds, excellent endurance/retention and allows strong Vdd fluctuations. The memory uses CMOS inverter read-out principle (C-Flash) and F-N injection for programming and erase with voltages below +5V. The memory is intended for RFID and advanced mobile applications requiring small/middle sized embedded memory modules.
The proceedings contain 17 papers. The topics discussed include: debugging Snomed CT using axiom pinpointing in the description logic EL+;leveraging SNOMED CT with a general purpose terminology server;LinKBase®...
The proceedings contain 17 papers. The topics discussed include: debugging Snomed CT using axiom pinpointing in the description logic EL+;leveraging SNOMED CT with a general purpose terminology server;LinKBase® and SNOMED: some distinct features and impact on NLP;exploiting fast classification of SNOMED CT for query and integration of health data;why do it the hard way? the case for an expressive description logic for SNOMED;SNOMED CT: browsing the browsers;interoperability of data models and terminology models: issues with using the SNOMED CT terminology;exploratory reverse mapping of ICD-10-CA to SNOMED CT;comparing SNOMED CT and the NCI thesaurus through semantic web technologies;essential SNOMED: simplifying SNOMED CT and supporting integration with health information models;representing clinical information using SNOMED clinical terms with different structural information models;and strategies for updating terminology mappings and subsets using SNOMED CT®.
This paper describes the problems with debugging tools for answer set programming, a declarative programming paradigm. Current approaches are difficult to use on most applications due to the considerable bottlenecks i...
详细信息
This paper describes the problems with debugging tools for answer set programming, a declarative programming paradigm. Current approaches are difficult to use on most applications due to the considerable bottlenecks in communicating the reasons to the user. In this paper we examine the reasons for this and suggest some possible future directions.
SNOMED CT medical vocabulary can be used to identify complementary features in a database. This functionality is used to develop a natural language processor (NLP) for PAIRS (Physician Assistant Artificial Intelligenc...
详细信息
SNOMED CT medical vocabulary can be used to identify complementary features in a database. This functionality is used to develop a natural language processor (NLP) for PAIRS (Physician Assistant Artificial Intelligence Reference System). Although about 99% of concepts in PAIRS are present in SNOMED CT some features missing in it makes it unacceptable for any diagnostic decision support system (DDSS). Here we show that implementation of another NLP along with SNOMED CT makes it practically useful.
X is an untyped continuation-style formal language with a typed subset that provides a Curry-Howard isomorphism for a sequent calculus for implicative classical logic. X can also be viewed as a language for describing...
详细信息
X is an untyped continuation-style formal language with a typed subset that provides a Curry-Howard isomorphism for a sequent calculus for implicative classical logic. X can also be viewed as a language for describing nets by composition of basic components connected by wires. These features make X an expressive platform on which many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for X;in order to demonstrate its expressive power, we will show how elaborate calculi can be embedded, such as the lambda-calculus, Bloo and Rose's calculus of explicit substitutions lambda x, Parigot's lambda mu and Curien and Herbelin's lambda mu mu. X was first presented in Lengrand (2003), where it was called the lambda xi-calculus. It can be seen as the pure untyped computational content of the reduction system for the implicative classical sequent calculus of Urban (2000).
Snomed ct is a large-scale medical ontology, which is developed using a variant of the inexpressive Description logic EL. Description logic reasoning can not only be used to compute subsumption relationships between S...
详细信息
Snomed ct is a large-scale medical ontology, which is developed using a variant of the inexpressive Description logic EL. Description logic reasoning can not only be used to compute subsumption relationships between Snomed concepts, but also to pinpoint the reason why a certain subsumption relationship holds by computing the axioms responsible for this relationship. This helps developers and users of Snomed ct to understand why a given subsumption relationship follows from the ontology, which can be seen as a first step toward removing unwanted subsumption relationships. In this paper, we describe a new method for axiom pinpointing in the Description logic EL+, which is based on the computation of so-called reachabilitybased modules. Our experiments on Snomed ct show that the sets of axioms explaining subsumption are usually quite small, and that our method is fast enough to compute such sets on demand.
Connectionist systems such as Radial Basis Function Neural Networks and similar architectures are commonly applied to solve problems of learning relations from available examples. To overcome their limits in clarity o...
详细信息
ISBN:
(纸本)9783540876557
Connectionist systems such as Radial Basis Function Neural Networks and similar architectures are commonly applied to solve problems of learning relations from available examples. To overcome their limits in clarity of representation, they are often interfaced with symbolic rule-based systems, provided that the information they have memorized can be interpreted. In this paper, an automatic implementation of a RBF-like system is presented using only gradual fuzzy rules learned by induction directly from training data. It is then shown that the same formalism, used with type-II truth values, can learn second-order, fuzzy relations.
暂无评论