Wednesday, October 22, 2014

 

 



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 131,906

110721. Reducing Communication Overhead In Distributed Logic Simulation Of Circuits - Amar Guettaf,Pirouz Bazargan-sabet
Distributed simulation represents an attractive and smart way of improving the verification speed of large VLSI circuits. Unfortunately, this inexpensive approach suffers from the low performance of the communication networks used to connect local workstations. In this paper, we present a partitioning algorithm that attempt to find a suitable balance between the communication and the execution load in a distributed simulator to enhance its speedup. The main features of this method are the use of logic replication to reduce the communication overhead and a realistic cost function that takes into account the activity of signals. Signals' activity can be obtained through a probabilistic evaluation. A distributed simulator implementing a conservative synchronization method has been used to...

110722. David N. Turner, An Teallach Limited,
Two different operational interpretations of intuitionistic linear logic have been proposed in the literature. The simplest interpretation recomputes non-linear values every time they are required. It has good memory-management properties, but is often dismissed as being too inefficient. Alternatively, one can memoize the results of evaluating non-linear values. This avoids any recomputation, but has weaker memory-management properties. Using a novel combination of type-theoretic and operational techniques we give a concise formal comparison of the two interpretations. Moreover, we show that there is a subset of linear logic where the two operational interpretations coincide. In this subset, which is sufficiently expressive to encode call-by-value lambda-calculus, we can have the best of both worlds: a simple...

110723. Implicit Coercions in Type Systems - Gilles Barthe
. We propose a notion of pure type system with implicit coercions. In our framework, judgements are extended with a context of coercions Delta and the application rule is modified so as to allow coercions to be left implicit. The setting supports multiple inheritance and can be applied to all type theories with Pi-types. One originality of our work is to propose a computational interpretation for implicit coercions. In this paper, we demonstrate how this interpretation allows a strict control on the logical properties of pure type systems with implicit coecions. 1 Introduction The increasing importance of mathematical software has been accompanied by a drift of mainstream mathematics towards mathematical...

110724. Accurate VHDL Delay and Power Characterization of CMOS Logic Cells - N. Dumitru,R. Nouta
This paper presents a model for characterizing delay and power for CMOS logic cells that accounts for input slope and output capacitance loading. A method for deriving the model parameters and VHDL modeling for simple logic gates is presented. The model makes feasible delay and power estimation at VHDL simulation speed, the errors of the model prediction are less than 5% of Spice results. 1 Introduction Analog circuit simulators suffer from severe memory and execution time constraints and are hence unsuitable for VLSI circuits. Logic and timing simulators are much faster, but their accuracy depends upon the accuracy of the model used for simulation. Usually, delay and power models used by logic simulators assume signal...

110725. Linear Space Induction in First Order Logic with RELIEFF - Uros Pompe,Igor Kononenko
Current ILP algorithms typically use variants and extensions of the greedy search. This prevents them to detect significant relationships between the training objects. Instead of myopic impurity functions, we propose the use of the heuristic based on RELIEF for guidance of ILP algorithms. At each step, in our ILP-R system, this heuristic is used to determine a beam of candidate literals. The beam is then used in an exhaustive search for a potentially good conjunction of literals. From the efficiency point of view we introduce interesting declarative bias which enables us to keep the growth of the training set, when introducing new variables, within linear bounds...

110726. An Algorithm for Exact Bounds on the Time Separation of Events in Concurrent Systems - Tod Amon,Henrik Hulgaard,Steven M. Burns,Gaetano Borriello
Determining the time separation of events is a fundamental problem in the analysis, synthesis, and optimization of concurrent systems. Applications range from logic optimization of asynchronous digital circuits to evaluation of execution times of programs for real-time systems. We present an efficient algorithm to find exact (tight) bounds on the separation time of events in an arbitrary process graph without conditional behavior. The algorithm is based on a functional decomposition technique that permits the implicit evaluation of an infinitely unfolded process graph. 1 Introduction In this paper, we derive an exact algorithm that determines tight upper and lower bounds on the separation in time of an arbitrary pair of system events. Depending on the level...

110727. A Proof-Theoretic Approach to Knowledge - Mariko Yasugi,Sobei H. Oda
rators K 1 and K 2 . It is essentially equivalent to the modal logic S4, with two neccesity operators. For technical reasons, we employ a sequential calculus. The cut elimination theorem for KL can be proved by following that of the propositional part of Gentzen's LK. Two of its consequences (elimination of 3 This work has been supported in part by Grant-in-Aid for Scientific Researches (No.10874024) and by RIMS y This work has been supported in part by Grant-in-Aid for Scienific Researches (No.09630018) knowledge operators and separation of formula sets) can be proved similarly to the corresponding lemmas in [1]. They serve as key lemmas in establishing various facts to solve the...

110728. Formal Real-Time Imagination - Madhura Nirkhe,Sarit Kraus
Formal real-time imagination is a term that may curiously describe the activities of a commonsense agent in a real-time setting in general, and in a tight deadline situation in particular. We briefly describe an `active-logic' mechanism that fits this description. Temporal projection is an essential component of realtime planning. We draw a parallel between imagination as we understand it in human context and the capacity of the automated agent to formulate mental images of possible scenarios and plans of action in the course of its reasoning. We outline a treatment of temporal issues of significance to a time-situated reasoning mechanism in a dynamic setting with deadlines. The Yale...

110729. There's No Substitute for Linear Logic - Philip Wadler
Surprisingly, there is not a good fit between a syntax for linear logic in the style of Abramsky, and a semantics in the style of Seely. Notably, the Substitution Lemma is valid if and only if !A and !!A are isomorphic in a canonical way. An alternative syntax is proposed, that has striking parallels to Moggi's language for monads. In the old syntax, some terms look like the identity that should not, and vice versa; the new syntax eliminates this awkwardness. 1 Introduction This paper has two purposes: to show that linear logic has no substitute, and to propose one. The first part presents a standard syntax and semantics...

110730. On Semantics of Algorithms with Continuous Time - Anatol Slissenko
We consider a class of algorithms with explicit continuous time, a logic which suffices to write requirement specifications for them in a way close to natural language, and, finally, the corresponding verification problem. Our main goal is to represent the whole problem in one logic. As algorithms we take block Gurevich machines [Gur95] over a signature with addition of reals, and as the logic we take an appropriate extension of the theory of real addition. A definition of semantics of algorithms of this type is given, without infinitesimals as compared to our previous one [BS97b], however under a condition not too much restricting for applications. Then we...

110731. Logical Foundations of Eval/Quote Mechanisms, and the Modal Logic S4 - Jean Goubault-larrecq
Starting from the idea that cut elimination is the precise meaning of program execution, we design two languages of constructions for the minimal logic S4, yielding -calculi with idealized versions of Lisp's eval and quote. The first, the S4 -calculus, is based on Bierman and De Paiva's proposal, and has all desirable logical properties, except for its non-operational flavor. The second, the evQ-calculus, is more complicated, but has a clear operational meaning: it is a tower of interpreters in the style of Lisp's reflexive tower. Remarkably, this language was developed from purely logical principles, but nonetheless provides some operational insight into eval/quote mechanisms. 1 Introduction Let's consider two dual questions. The first is: is there...

110732. Finer Control of Weakening and Contraction: Towards a Separated-Linear Lambda Calculus (Summary) - John Maraist
nisms by which we introduce the copying or discarding of terms. A term is discarded when it is substituted for a variable which appears only on the left side of a typing judgement, which can occur only as the result of applying a weakening rule; a term is duplicated when it is substituted for a variable which appears more than once on the right side of a typing judgement, which can occur only by a contraction rule. In the substructural lambda calculi I [3], A and L [8], the use of (respectively) weakening, contraction and both are simply banned. These systems are not suOEcient here: while...

110733. Verification of Logic Programs with Delay Declarations - Krzysztof R. Apt
. Logic programs augmented with delay declarations form a higly expressive programming language in which dynamic networks of processes that communicate asynchronously by means of multiparty channels can be easily created. In this paper we study correctness these programs. In particular, we propose proof methods allowing us to deal with occur check freedom, absence of deadlock, absence of errors in presence of arithmetic relations, and termination. These methods turn out to be simple modifications of the corresponding methods dealing with Prolog programs. This allows us to derive correct delay declarations by analyzing Prolog programs. Finally, we point out difficulties concerning proofs of termination. Notes. The research of the first author was...

110734. Tractable Approximate Deduction using Limited Vocabularies - Mukesh Dalal,David W. Etherington
A new approach to tractable deduction from an expressive knowledge base is presented that approximates formulae by automatically mapping them to some restricted language. Various mappings and their properties are discussed, and an anytime algorithm to compute approximations is presented. Several published approaches prove to be special instances of ours. To illustrate this, our formalism is used to formalize hierarchical knowledge bases, and to extend them by allowing negation and mutual exclusion. We believe this to be the first comprehensive theoretical framework for approximate reasoning. 1 Introduction It is well known that reasoning with a knowledge representation system becomes more difficult as the representation language becomes more expressive [ Levesque and Brachman, 1985 ] . Reasoning is apparently...

110735. Handling Infeasible Specifications of Cryptographic Protocols - Li Gong
In the verification of cryptographic protocols along the approach of the logic for authentication by Burrows, Abadi, and Needham, it is possible to write a specification which does not faithfully represent the real world situation. Such a specification, though impossible or unreasonable to implement, can go undetected and be verified to be correct. It can also lead to logical statements that do not preserve causality, which in turn can have undesirable consequences. Such a specification, called an infeasible specification here, can be subtle and hard to locate. This note shows how the logic of cryptographic protocols by Gong, Needham, and Yahalom can be enhanced with a notion of eligibility to preserve causality of...

110736. Automated Deduction in a Graphical Temporal Logic - L. E. Moser,P. M. Melliar-smith,Y. S. Ramakrishna,G. Kutty,L. K. Dillon
. Real-Time Graphical Interval Logic is a modal logic for reasoning about time in which the basic modality is the interval. The logic differs from other logics in that it has a natural intuitive graphical representation that resembles the timing diagrams drawn by system designers. We have developed an automated deduction system for the logic, which includes a theorem prover and a user interface. The theorem prover checks the validity of proofs in the logic and produces counterexamples to invalid proofs. The user interface includes a graphical editor that enables the user to create graphical formulas on a workstation display, and a database and proof manager that tracks...

110737. Designing Advanced Databases Using Dependency Graph Conducted Schema Transformation Algorithm (Extended Abstract) - Patrick Van Bommel
Tecnical Note CSI-N9703, March 1997 Current address: Dept. of Information Systems, University of Nijmegen, Toernooiveld 1, NL-6525 ED Nijmegen, The Netherlands. Email: gyurik@cs.kun.nl Contents 1 Introduction 3 2 Framework for algorithmic schema transformation 4 2.1 Transformation dependency graphs : : : : : : : : : : : : : : : 5 2.2 The transformation algorithm : : : : : : : : : : : : : : : : : : 7 3 From conceptual models to OO databases 9 3.1 Approach : : : : : : : : : : : : : : : : : : : : : :...

110738. A Three-Valued Linear Temporal Logic for Reasoning about Concurrency - Beata Konikowska
this paper we choose the second one, since it allows to preserve most intuitions and methods connected with the classical case, including classical tautologies on formula level, as well as the classical method of Hilbert-type axiomatization together with the standard proof of its completeness by canonical model construction. 3 Syntax and semantics of the language

110739. Handling Database Updates in Two-dimensional Temporal Logic - Marcelo Finger
This paper deals with the description of the evolution of the understanding of the history of a particular world. We have particular interest in describing certain problems that occur in database systems due to updates. For this purpose, we introduce a two-dimensional temporal logic as a formalism which enables the description of both the history and the evolution of the beliefs about the history. The historical dimension describes the history of the world according to a certain belief. The belief dimension describes the evolution of those beliefs. The historical dimension is then associated with an historical database, and transactions in the database are associated with changes in belief. Besides describing...

110740. Spatial Logic and the Complexity of Diagrammatic Reasoning - Oliver Lemon,Ian Pratt
. Researchers have sought to explain the observed "efficacy" of diagrammatic reasoning (DR) via the notions of "limited abstraction" and inexpressivity [17, 20]. We argue that application of the concepts of computational complexity to systems of diagrammatic representation is necessary for the evaluation of precise claims about their efficacy. We show here how to give such an analysis. Centrally, we claim that recent formal analyses of diagrammatic representations (DRs) (eg: [14]) fail to account for the ways in which they employ spatial relations in their representational work. This focus raises some problems for the expressive power of graphical systems, related...

 

Busque un recurso