Friday, August 28, 2015



Soy un nuevo usuario

Olvidé mi contraseña

Entrada usuarios

Lógica Matemáticas Astronomía y Astrofísica Física Química Ciencias de la Vida
Ciencias de la Tierra y Espacio Ciencias Agrarias Ciencias Médicas Ciencias Tecnológicas Antropología Demografía
Ciencias Económicas Geografía Historia Ciencias Jurídicas y Derecho Lingüística Pedagogía
Ciencia Política Psicología Artes y Letras Sociología Ética Filosofía

rss_1.0 Clasificación por Disciplina

Nomenclatura Unesco > (11) Lógica

Mostrando recursos 110,721 - 110,740 de 148,687

110721. Smart Memory: The Memory Processor Model - Tony R. Martinez
This paper overviews and proposes a class of smart memory devices called the memory processor model. Smart memory entails the tight coupling of memory and logic. The model seeks to alleviate the von Neumann bottleneck, take advantage of technology trends, improve overall system speed, and add encapsulation advantages. Speed is increased through locality of processing, communication savings, higherlevel functionality, and parallelism. Parallelism is exploited at both the micro and macro levels. Data objects are accessed through descriptors, which give the memory a meta-knowledge concerning the objects, allowing for nontraditional access mechanisms. Both data types and operations are programmable. Innovative processing schemes, coupled with emerging technology densities, allow for substantial speed-up...

110722. Proofs and Expressiveness in Alethic Modal Logic - Maarten Rijke,Heinrich Wansing
Introduction Alethic modalities are the necessity, contingency, possibility or impossibility of something being true. Alethic means `concerned with truth'. [28, p. 132] The above dictionary characterization of alethic modalities states the central notions of alethic modal logic: necessity, and other notions that are usually thought of as being definable in terms of necessity and Boolean negation: impossibility, contingency, and possibility. The syntax of modal propositional logic is inductively defined over a denumerable set of sentence letters p 0 , p 1 , p 2 , . . . as follows: A ::= p | A | (A # B) | #A The other Boolean operations (#, #, #, # and #) are defined as usual. A formula
110723. Globalization and its Implications: The Size and Location of Manufacturing Sector Export Firms in SC - William A. Ward
logic would suggest that scale requirements would be greater for agricultural than for most manufactured goods exports because of the higher policy risk and spoilage risk (which tend to interplay with each other) associated with the former. W. Ward Globalization---November 15, 2000 21 regional trade associations around the state, and the SC World Trade Center at Charleston. By working in collaboration with these Partners, the CIT seeks to identify, produce and disseminate results from a program of "rigorous and relevant research" that would be both rigorously conducted and immediately applicable to trade and economic development issues facing South Carolina. By simultaneously engaging our faculty, graduate students and undergraduate students...

110724. A Proof of Craig's Interpolation Theorem in Coq - In Coq,James Mckinna,Healfdene Goguen
INTRODUCTION 1 1 Introduction The aim of this project was to give a formal proof in type theory of some rst order syntactic theorems, as Craig's interpolation or cut elimination. As I knew neither Lego nor Coq, my rst work had been to learn one of them : James and Healfdene adviced me to learn Coq, because I know Caml, which would allow me to program tactics. First order logic is a usual formalization of some mathematical theories, one of the project motivation is to try to express it in a formalized metalanguage : it may help to nd the crucial keys of proofs and so to better understand...

110725. Executable Protocol Specification in ESL - E. Clarke,S. German,Y. Lu,H. Veith,D. Wang,Tu Vienna
Hardware specifications in English are frequently ambiguous and often self-contradictory. We propose a new logic ESL which facilitates formal specification of hardware protocols. Our logic is closely related to LTL but can express all regular safety properties. We have developed a protocol synthesis methodology which generates Mealy machines from ESL specifications. The Mealy machines can be automatically translated into executable code either in Verilog or SMV. Our methodologyexploits the observation that protocols are naturally composed of many semantically distinct components. This structure is reflected in the syntax of ESL specifications. We use a modified LTL tableau construction to build a Mealy machine for each component. The Mealy machines are...

110726. Specification of Logic Programming Languages from Reusable Semantic Building Blocks - J. E. Labra Gayo,J. M. Cueva Lovelle,M. C. Luengo Dez,A. Cernuda Del Ro
We present a Language Prototyping System that facilitates the modular development of interpreters from independent semantic building blocks. The abstract syntax is modelled as the fixpoint of a pattern functor which can be obtained as the sum of functors. For each functor we define an algebra whose carrier is the computational structure. This structure is obtained as the composition of several monad transformers to a base monad, where each monad transformer adds a new notion of computation. When the abstract syntax is composed from mutually recursive categories, we use many-sorted algebras. With this approach, the prototype interpreters are automatically obtained as a catamorphism over the defined algebras. As an example, in...

110727. Deductive Databases --- Where to Now? - Mengchi Liu
Deductive databases result from the integration of database and logic programming techniques. It combines the benefits of these two approaches, such as representational and operational uniformity, recursion, declarative querying, efficient secondary storage access, etc. However, significant problems remain inherent in this synthesis. There are four broad areas where problems are apparent. The first problem area is how to naturally represent complex values consists of nested tuples and sets. The second problem area is how to incorporate object-oriented features into deductive framework. The third problem area is how to naturally deal with higher-order features in deductive databases. The last is the area of updates. This paper elaborates these problems,...

110728. Specification and Verification of Synchronous Hardware using - Ji He,Kenneth J. Turner
This paper investigates specification and verification of synchronous circuits using DILL (Digital Logic in LOTOS). After an overview of the DILL approach, the paper focuses on the characteristics of synchronous circuits. A more constrained model is presented for specifying digital components and verifying them. Two standard benchmark circuits are specified using this new model, and analysed by the CADP toolset (Csar/Aldbaran Development Package).

110729. Simplified Heterogeneous Specification - Till Mossakowski
Existing approaches to heterogeneous specifications deal with the integration of different logics via logic projections, logic encodings and bridges of proof calculi. We show how to combine these approaches into a single, simplified approach.

110730. Planning with Different Forms of Domain-Dependent Control Knowledge - An Answer Set Programming Approach - Tran Cao Son,Chi Baral
In this paper we present a declarative approach to adding domain-dependent control knowledgef or Answer Set Planning (ASP). Our approach allows di#erent types of domain-dependent control knowledge such as hierarchical, temporal, or procedural knowledge to be represented and exploited in parallel, thus combining the ideas of control knowledge in HTN-planning, GOLOG-programming, and planning with temporal knowledge into ASP. To do so, we view domain-dependent control knowledge as sets of independent constraints. An advantageof this approach is that domain-dependent control knowledge can be modularly f ormalized and added to the planning problem as desired. We define a set of constructsf- constraint representation and provide a set of domainindependent logic programming rulesf or checking constraint satisfhH ion. 1

110731. Model Checking Security Protocols Using a Logic of Belief - Scientifica E Tecnologica,M. Benerecetti,F. Giunchiglia
In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. The idea underlying the approach is to treat separately the temporal evolution and the belief aspects of principals. Therefore, when we consider the temporal evolution, belief formulae are treated as atomic propositions; while the fact that principal A has beliefs about another principal B is modeled as the fact that A has access to a representation of B as a process. As a motivating example, we use the framework proposed to formalize the Andrew protocol.

110732. IRAM Design for Multimedia Applications - Bum-sik Kim,Yun Ho Choi,Lee-sup Kim
There are strong demands for high speed and low power to realize systems on silicon. However, the current circuit design technologies for MPU and DRAM are based on their own optimized process technologies. It is necessary modify the circuit design technology for embedded memory logic after reviewing process technologies of MPU and DRAM. In this paper, we propose the modified design concept for IRAM for multimedia applications. After scrutinizing an example of multimedia applications, we propose a new IRAM architecture for multimedia applications. We are currently designing IRAM system which executes DCT of MP@ML in MPEG2 at 72.6MHz with 0.35m CMOS EML (Embedded Memory and Logic) process with 4-metal layers. Also, we...

110733. Evolving Games and Essential Nets for Ane Polymorphism - Ane Polymorphism,A. S. Murawski,C. -h. L. Ong,Wolfson Building
This paper presents a game model of Second-order Intuitionistic Multiplicative Ane Logic (IMAL2). We extend Lamarche's essential nets to the second-order ane setting and use them to show that the model is fully and faithfully complete.

110734. Polarized and Focalized Linear and Classical Proofs - Olivier Laurent,Myriam Quatrini,Iml-cnrs Marseille,Lorenzo Tortora De Falco,Roma Iii
We give the precise correspondence between polarized linear logic and polarized classical logic. The properties of focalization and reversion of linear proofs [AP91, Gir91a, DJS97] are at the heart of our analysis: we show that the tq-protocol of normalization (dened in [DJS97]) for the classical systems LK pol and LK ; pol perfectly ts normalization of polarized proof-nets. In section 6, some more semantical considerations allow to recover LC as a renement of multiplicative LK pol . MSC: 03F05; 03F07; 03F52 Keywords: Classical Logic, Linear Logic, Cut-Elimination, Proof-Nets, Denotational Semantics, Polarization, Focalization, Reversion.

110735. Poset-valued sets or How to build models for Linear Logics - Andrea Schalk,Valeria De Paiva
We describe a method for constructing models of linear logic based on the category of sets and relations. The resulting categories are generally not degenerate, in particular the are not compact closed nor do they have biproducts. The construction is simple, relying on the structure of a poset to avoid degeneracy. A number of wellknown models, for example coherence spaces and hypercoherences, are instances of this method. Key words: Linear Logic; categorical models 1

110736. Relating Disjunctive Logic Programs to Default Theories - Chiaki Sakama,Katsumi Inoue
This paper presents the relationship between disjunctive logic programs and default theories. We first show that Bidoit and Froidevaux's positivist default theory causes a problem in the presence of disjunctive information in a program. Then we present a correct transformation of disjunctive logic programs into default theories and show a one-to-one correspondence between the stable models of a program and the extensions of its associated default theory. We also extend the results to extended disjunctive programs and investigate their connections with Gelfond et al's disjunctive default theory, autoepistemic logic, and circumscription.

110737. Logic-based Knowledge Discovery in Databases - Fosca Giannotti,Mirco Nanni,Dino Pedreschi
this paper, are extensively studied in [2, 4, 5, 10]

110738. An Ontology For Standards - J. R. Velman,E. R. Widmann
The paper continues the exploration of standards that the authors initiated in [1] and continued in [2] and [3]. It provides an ontology for standards---a specification of the things and relationships relevant to the topic of standards. The ontology is presented using the ISO standard graphical language, EXPRESS-G. It uses concepts from mathematical logic to clarify the content, meaning, and use of standards. Characteristics and elements of standards that are independent of any particular usage of the standard are defined. The subject matter of standardization is classified and a taxo nomy is presented. Instances of earliest use of each part of the taxonomy are described. The means of establis hing standards is discussed,...

110739. Rasiowa-Sikorski Deduction Systems - Foundations and Applications - Beata Konikowska
Introduction The aim of this tutorial is to present a powerful and exible, yet simple methodology of developing deduction systems for various logics based on the analysis of their semantics. The paper will present a general outline of this methodology, and show examples of its applications to various brands of computer science logics. The said methodology is inherently connected with the semantics of the given logic, and its key concept is to obtain an adequate and complete proof mechanism for the logic in a systematic way from the said semantics. This is achieved by "mirroring" the semantics of all the logical constructs (connectives, quantiers, modalities, . . . ) through...

110740. A Correct, Precise and Efficient Integration of Set-Sharing, Freeness and Linearity for the Analysis of Finite and Rational Tree Languages - Patricia M. Hill,Enea Zaanella,Roberto Bagnara
It is well-known that freeness and linearity information positively interact with aliasing information, therefore allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper we present a novel combination of set-sharing with freeness and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in [3] also applies to this abstract domain combination: this...


Busque un recurso