Sunday, March 29, 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 140,166

110721. Verifying Privacy Enhanced Mail Functions with Higher Order Logic - Dan Zhou,Shiu-kai Chin
. Security properties such as privacy, authentication, and integrity are of increasing importance to networked systems([KAU]). Systems with security requirements typically must operate with a high degree of confidence. We show how the message structures of Privacy Enhanced Mail (PEM, [LIN, BAL]) and the functions on PEM structures have the desired implementation -independent security properties. Higher-order logic ([AND]) and the HOL theorem-prover([GOR]) are used to precisely relate security properties to system specifications. The structures of MIC-CLEAR and ENCRYPTED messages are modeled as tuples of fields. Each of these fields is modeled as a type which takes only a limited set of values as valid ([MEL]). Security functions for checking privacy,...

110722. Automatic Verification of Real-time Systems with Discrete Probability Distributions - Marta Kwiatkowska,Roberto Segala
We consider the timed automata model of [3], which allows the analysis of realtime systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, it is often desirable to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, two approaches to model checking are introduced for this model. The first uses the algorithm of [6] to provide a verification technique for our model against temporal logic properties which can refer both to timing properties and probabilities. The second, generally more...

110723. Using Abduction to Evolve Inconsistent Requirements Specifications - Bashar Nuseibeh,Alessandra Russo
Requirements specifications are often inconsistent. Inconsistencies may arise because multiple conflicting requirements are embodied in these specifications, or because the specifications themselves are in a transient stage of evolutionary development. In this paper we argue that such inconsistencies, rather than being undesirable, are actually useful drivers for changing the requirements specifications in which they arise. We present a formal technique to reason about inconsistency handling changes. Our technique is an adaptation of logical abduction -- adapted to generate changes that address some specification inconsistencies, while leaving others. We represent our specifications in quasi-classical (QC) logic -- an adaptation of classical logic that allows continued reasoning in the...

110724. Extending Fuzzy Logics to Support Decisions - Wojciech Jamroga
. In this paper a concept of evaluation schema for uncertain statements is proposed. The aim is to represent and process knowledge and to support decision making under uncertainty, involving the information with unmeasurable uncertainty in the reasoning process. This 'uncertainty logic' is based on fuzzy logics and L/ukasiewicz three-valued logic, but it's underlied by a richer structure that makes more subtle analysis of statements possible. The logic is a kind of L-fuzzy logic formally. However, its ontological motivations are different. Keywords: knowledge representation, reasoning under uncertainty, decision making, fuzzy logics, three-valued logic. 1 Motivations 1.1 Philosophical Motivations According to (Klir & Folger 1988), situations of uncertainty arise either...

110725. Logic Programming with Linear Logic - Michael David Winikoff
Programming languages are the basic tools of computer science. The design of a good programming language is a trade-off between many factors. Perhaps the most important and difficult trade-off is between execution efficiency and programmer efficiency. Higher level languages reduce the amount of work the programmer has to do; however they have, to date, been less efficient than lower level languages. That lower level languages are necessarily more efficient is a piece of folklore which is under attack -- higher level languages are constantly coming closer to the performance of the lower level languages. A consequence of this constantly closing performance gap is that the abstraction level of...

110726. Transition Density, A New Measure of Activity in Digital Circuits - Farid N. Najm
Reliability assessment is an important part of the design process of digital integrated circuits. We observe that a common thread that runs through most causes of run-time failure is the extent of circuit activity, i.e., the rate at which its nodes are switching. We propose a new measure of activity, called the transition density, which may be defined as the "average switching rate" at a circuit node. Based on a stochastic model of logic signals, we also present an algorithm to propagate density values from the primary inputs to internal and output nodes. To illustrate the practical significance of this work, we demonstrate how the density values...

110727. Holcf = Hol + Lcf - Olaf Muller,Tobias Nipkow,David Von Oheimb,Oscar Slotosch
HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF supports standard domain theory (in particular fixpoint reasoning and recursive domain equations) but also coinductive arguments about lazy datatypes. This paper describes in detail how domain theory is embedded in HOL and presents applications from functional programming, concurrency and denotational semantics. 1 Introduction HOLCF is a logic for reasoning about functional programs. It provides arbitrary forms of recursion (via a fixpoint operator) and a package for defining datatypes. The latter caters for infinite objects,...

110728. Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic - James Harland,Tatjana Lutovac,Michael Winikoff
. A key property in the definition of logic programming languages is the completeness of goal-directed proofs. This concept originated in the study of logic programming languages for intuitionistic logic in the (single-conclusioned) sequent calculus LJ, but has subsequently been adapted to multiple-conclusioned systems such as those for linear logic. Given these developments, it seems interesting to investigate the notion of goal-directed proofs for a multiple-conclusioned sequent calculus for intuitionistic logic, in that this is a logic for which there are both single-conclusioned and multiple-conclusioned systems (although the latter are less well known). In this paper we show that the language obtained for the multiple-conclusioned system differs from that...

110729. Fuzzy Selection and Blending of Behaviors for Situated Autonomous Agent - Franois Michaud,Grard Lachiver,Chon Tam,Le Dinh
Intelligent control is a field of research attempting to attain demanding control goals in complex systems. To do so, many methods and theories must be combined and used efficiently. We propose a new control architecture that tries to unify the principles and characteristics associated with intelligence. This architecture uses behaviors as its basic control components. These behaviors are selected dynamically and their actions are combined according to the intentions of the agent. Introspection of its reactions is one major new ability given to the agent by this architecture. A simulated world for mobile robots is used to validate the characteristics and the principles associated with our proposed architecture. This article focuses on the...

110730. Testing Attribute Grammars - Universitt Rostock Fachbereich Informatik
Fundamental notions for testing attribute grammars are developed. Two dimensions are explored. The structural dimension focuses on the context-free grammar part of an attribute grammar, whereas the semantic dimension is concerned with attributes, attribute types, conditions, and computations. In both dimensions, and also for the combination of them, we are interested in coverage notions, test set criteria (e.g., minimum test sets), and test set generation. The described framework builds upon abstract interpretation technology, and search algorithms. The approach is also applicable to some other representatives of the declarative paradigm, such as logic programming and term rewriting. Examples illustrate that the...

110731. Formal Development of Secure Email - Dan Zhou,Joncheng C. Kuo,Susan Older,Shiu-kai Chin
Developing systems that are assured to be secure requires precise and accurate descriptions of specifications, designs, implementations, and security properties. Formal specification and verification have long been recognized as giving the highest degree of assurance. In this paper, we describe a software development process that integrates formal verification and synthesis. We demonstrate this process by developing assured sender and receiver C++ code for a secure electronic mail system, Privacy Enhanced Mail. We use higher-order logic for system-requirements specification, design specifications and design verification. We use a combination of higher-order logic and category theory and tools supporting these formalisms to refine specifications and synthesize code. Much of our work is applicable to other secure email...

110732. Pipelined DSP Design with a True Single-Phase Energy-Recovering Logic Style - Suhwan Kim,Marios C. Papaefthymiou
We recently invented a true single-phase energy-recovering circuit family, called TSEL, that relies on a cross-coupled latch structure and two DC reference voltages to achieve low energy consumption for a broad range of operating frequencies. In this paper, we explore the application of TSEL to the design of low-energy DSP circuits. Specically, we describe and evaluate a 6,768-transistor, pipelined TSEL module that performs the 8-point Hadamard Transform. In layout simulations with a standard 0.5m CMOS technology, our TSEL module functions correctly for operating frequencies in excess of 280MHz. Above 40MHz, our TSEL design is more energy-ecient than any other energy-recovering alternative with a similar cross-coupled latch structure....

110733. Linear Relaxations and Reduced-Cost Based Propagation of Continuous Variable Subscripts - Greger Ottosson,Erlendur S. Thorsteinsson
In hybrid solvers for combinatorial optimization, combining Constraint (Logic) Programming (CLP) and Mixed Integer Programming (MIP), it is important to have tight connections between the two domains. We extend and generalize previous work on automatic linearizations and propagation of symbolic CLP constraints that cross the boundary between CLP and MIP. We also present how reduced costs from the linear programming relaxation can be used for domain reduction on the CLP side. Computational results comparing our hybrid approach with pure CLP and MIP on a configuration problem show significant speed-ups.

110734. SimNet, A Tool for Simulation with Application to Project Network Analysis - Fredrick Von Schoultz,Aimo Torn
Simulation Nets (SN) are Petri Nets extended for convenient modelling of discrete event simulation problems. The extensions included are zero testing, firing time for transitions, or-logic and net hierarchies. The tool SimNet accepts a text equivalence of SNs and performs the simulation implied by the SN model. Validation is facilitated by providing trace, animation, and statistics collection. An application to project network analysis is described. Key words: Petri Nets, discrete event simulation, Simula, Simulation Nets, project networks I. Introduction Simulation Nets or as they then were called, Simulation Graphs, were introduced in 1981 as a simulation modelling tool based on extended Petri Nets [Torn 1981]. The first computer tool, Simnex, capable of reading a single Simulation Net and...

110735. Single-Phase Source-Coupled Adiabatic Logic - Suhwan Kim,Marios C. Papaefthymiou
Adiabatic circuits offer a promising alternative to conventional circuitry for low energy design. Their operation is nevertheless subject to fundamental energy-speed trade-offs, just like any other physical realization of boolean logic. Thus, adiabatic circuits with very low energy consumption at low frequencies fail to function at high operating frequencies. Conversely, high-speed adiabatic circuits tend to be dissipative at low clock rates. This paper describes SCAL, a single-phase source-coupled adiabatic logic family that operates efficiently across a wide range of operating frequencies. In layout-based simulations with 0.5m CMOS process parameters, pipelined carry-lookahead adders developed in our logic function correctly from 10MHz up to 280MHz. Our SCAL adders are less dissipative than corresponding designs...

110736. A Kleene Analysis of Mobile Ambients - Flemming Nielson,Hanne Riis Nielson,Mooly Sagiv
We show how a program analysis technique originally developed for C-like pointer structures can be adapted to analyse the hierarchical structure of processes in the ambient calculus. The technique is based on modeling the semantics of the language in a two-valued logic; by reinterpreting the logical formulae in Kleene's three-valued logic we obtain an analysis allowing us to reason about may as well as must properties. The correctness of the approach follows from a general Embedding Theorem for Kleene's logic; furthermore embeddings allow us to reduce the size of structures so as to control the time and space complexity of...

110737. BI as an Assertion Language for Mutable Data Structures - Peter W. O'hearn,Samin Ishtiaq
Reynolds has recently developed a logic for reasoning about mutable data structures, where pre- and post-conditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of O'Hearn and Pym. We begin by giving a model in which the law of the excluded middle holds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to Kripke's translation of intuitionistic logic into the modal logic S4. We also consider the question of completeness of...

110738. Constructing Conditional Plans by a Theorem-Prover - Jussi Rintanen
The research on conditional planning rejects the assumptions that there is no uncertainty or incompleteness of knowledge with respect to the state and changes of the system the plans operate on. Without these assumptions the sequences of operations that achieve the goals depend on the initial state and the outcomes of nondeterministic changes in the system. This setting raises the questions of how to represent the plans and how to perform plan search. The answers are quite different from those in the simpler classical framework. In this paper, we approach conditional planning from a new viewpoint that is motivated by the use of satisfiability algorithms in classical...

110739. Computationally Grounded Theories of Agency - Michael Wooldridge
In this paper, I motivate, define, and illustrate the notion of computationally grounded theories of agency. A theory of agency is said to be computationally grounded if we can give the theory an interpretation in terms of some concrete computational model. This requirement is essential if we are to claim that the theories we develop can be understood as expressing properties of real multiagent systems. After introducing and formally defining the concept of a computationally grounded theory of agency, I illustrate the idea with reference to VSK logic, a formalism for reasoning about agent systems that has a semantics defined with respect to an automata-like model of agents. VSK logic is...

110740. Model Checking in CLP - Giorgio Delzanno,Andreas Podelski
. We show that Constraint Logic Programming (CLP) can serve as a conceptual basis and as a practical implementation platform for the model checking of infinite-state systems. Our contributions are: (1) a semantics-preserving translation of concurrent systems into CLP programs, (2) a method for verifying safety and liveness properties on the CLP programs produced by the translation. We have implemented the method in a CLP system and verified well-known examples of infinitestate programs over integers, using here linear constraints as opposed to Presburger arithmetic as in previous solutions. 1 Introduction Automated verification methods can today be applied to practical systems [McM93]. One reason for this success is that implicit representations of finite...

 

Busque un recurso