Friday, August 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 129,758

110721. A Calculus Supporting Structured Proofs - I. Dahn,Andreas Wolf
: Proofs in standard logical calculi have a simple structure (mostly a sequence, tree or set of related formulas). Therefore, formal proofs are hard to understand or to present in an intelligible way. The Block Calculus for first order logic introduced in this paper is a variant of natural deduction that has highly structured proofs. These proofs can be presented in many ways by hiding blocks of subproofs. Moreover it can be easily extended by other calculi. We characterize the semantics of incomplete proof structures in the Block Calculus and prove it's soundness and completeness. Contents 1. Introduction 1 2. Some Definitions 3 3. Rules 5 4. Examples 7 5. Completeness and...

110722. Applications of Circuit Probability Computation Using Decision Diagrams - M. A. Thornton
Digital circuit output probabilities provide meaningful information regarding the behavior of combinational logic circuits. The computation of the probability values can be computationally expensive when Boolean equations or netlists are used. When the circuits are represented by compact decision diagrams (DD), efficient algorithms exist for determining the probability values. The use of the probabilities based on decision diagram representations are examined here. Specifically, research results of investigations into spectra computation, synthesis, symmetry detection and DD reordering are surveyed. 1 Introduction The circuit output probability for a combinational logic circuit can be defined as the probability that a given output will yield a logical-1 value given the distributions of the inputs. These probability values have proven to be...

110723. Modelling Garbage Collection Algorithms - Howard Bowman,John Derrick,Richard Jones
We show how abstract requirements of garbage collection can be captured using temporal logic. The temporal logic specification can then be used as a basis for process algebra specifications which can involve varying amounts of parallelism. We present two simple CCS specifications as an example, followed by a more complex specification of the cyclic reference counting algorithm. The verification of such algorithms is then briefly discussed. Keywords: Concurrency, garbage collection, temporal logic, CCS. 1 Introduction The memorymanagement of simple static programming languages, such as Fortran, can be handled entirely by the compiler. The location of all variables can be fully determined at compile-time and no run-time support for memory...

110724. Retrieval of Complex Objects Using a Four-Valued Logic - Thomas Rolleke,Norbert Fuhr
The aggregated structure of documents plays a key role in full-text, multimedia, and network Information Retrieval (IR). Considering aggregation provides new querying facilities and improves retrieval effectiveness. We present a knowledge representation for IR purposes which pays special attention to this aggregated structure of objects. In addition, further features of objects can be described. Thus, the structure of full-text documents, the heterogeneity and the spatial and temporal relationships of objects typical for multimedia IR, and meta information for network IR are representable within one integrated framework. The model we propose allows for querying on the content of documents (objects) as well as on other features. The query result may contain objects having different types....

110725. Non-Terminating Processes in the Situation Calculus - Eugenia Ternovskaia,Ray Reiter
this paper -- an office coffee-delivery robot might be implemented as an infinite loop in which the robot responds to exogenous requests for coffee that are maintained on a queue. Since a future coffee request is always possible, the program never terminates. As is the case for more conventional programs, we want some reliability assurances for robot controllers. This paper describes the approach being taken by our Cognitive Robotics Group to expressing and proving properties of non-terminating programs expressed in GOLOG, a high level logic programming language for modeling and implementing dynamical systems. The kinds of properties we have in mind are traditional in computer science: liveness,...

110726. Iterative Combinational Logic Synthesis Techniques Using Spectral Data - Mitchell Aaron Thornton,V. S. S. Nair
The spectral information of a Boolean function yields data regarding the correlation between the input variables and the output of the function. This paper introduces a spectral based methodology for combinational logic synthesis using linear transforms. An analysis of the properties of the spectra obtained from these transforms is provided and a synthesis algorithm using spectral techniques is presented. This result is significant since it provides an algebraic method for including the XOR gate in the synthesis process without resorting to manipulation of symbolic Boolean equations. 1 Introduction The design and development of digital systems is becoming increasingly complex and automated. With the evolution of greater amounts of circuitry...

110727. Fault Injection for Logic Synthesis Design using VHDL 1 of 8 - Todd A. Delong,Anup K. Ghosh,Barry W. Johnson,Joseph A. Profeta
Fault injection provides a method of assessing the dependability of a system under test. Traditionally fault injection is employed near the end of the design process after hardware and software prototypes have been developed. In order to eliminate costly re-designs near the end of the design process, a methodology for performing fault injection throughout the design process is described in this paper. This methodology incorporates a fault injection technique that can be used with any VHDL model, including behavioral, synthesizeable VHDL models. The technique separates the fault-free VHDL descriptions from the fault injection process so that existing models can be used with minimal changes to the existing...

110728. Asynchronous Pipeline Design using GaAs PDLL Logic and new CMOS dynamic techniques - Shannon V. Morton,Michael J. Liebelt
We explore the potential for extremely high asynchronous logic performance in CMOS and GaAs dynamic logic structures. By using a new class of GaAs dynamic logic, Pseudo-Dynamic Latched Logic, we develop asynchronous control structures capable of high-speed operation. We show how these techniques can be used for CMOS design, and give performance estimates. I Introduction Asynchronous approaches have long been touted as the ideal replacement for synchronous designs when clock skew problems and power consumption become unmanageable. However, the lack of asynchronous method acceptance seems to indicate that these views are not shared by the design community as a whole. This is primarly due to the lower performance level offered by asynchronous solutions in a...

110729. Last Parallel Call Optimization and Fast Backtracking in And-parallel Logic Programming Systems - Tang Dongxing,Enrico Pontelli,Manuel Carro,Gopal Gupta
In this paper we present a novel optimization called Last Parallel Call Optimization. The last parallel call optimization can be regarded as an extension of last call optimization, found in sequential systems, to and parallel systems. The last parallel call optimization leads to improved time and space performance for a majority of and-parallel programs. The last parallel call optimization is presented in detail in this paper and its advantages discussed at length. The last parallel call optimization can be incorporated in a parallel system (such as RAPWAM) through relatively minor modifications to the runtime machinery. We also present some experimental...

110730. Foundations Of Temporal Query Languages - David Toman
Temporal Databases are repositories of information dependent on time. The major difference from standard, e.g., relational database systems, is the need of storing possibly infinite objects, e.g., time spans. In recent years, there have been numerous proposals that introduce time into standard relational systems. Unfortunately, most of the attempts have been based on ad-hoc extensions of existing database systems and query languages, e.g., TQUEL and TSQL. Such extensions often create many problems, when precise semantics needs to be developed, if one exists at all. In a recent survey by J. Chomicki, a clean way of defining temporal databases based on logic was proposed. This methodology views temporal databases...

110731. Temporal Databases - Jan Chomicki,David Toman
ing of Temporal Databases and Temporal Query Languages. We briefly survey the classical results. However, the main emphasis is on recent developments in the area of temporal databases. In the light of several recent results [Abiteboul et al., 1996, Chomicki and Kuper, 1995, Chomicki et al., 1996, Kanellakis et al., 1995, Toman and Niwinski, 1996, Toman, 1996, Toman, 1997] many of the above issues have taken an unexpected turn and the correctness of several mainstream approaches has to be reevaluated. 1 In many temporal data models, new features are added without considering their interaction with existing features. 2 Detailed Outline of the Tutorial 1. Introduction temporal domains temporal dimensions of data 2. Temporal...

110732. Efficient Integration of Declarative Paradigms into Symbolic Computation Systems - Georgios Grivas
. This paper describes the efficient integration of the functional, logic and constraint paradigms into symbolic computation systems. Moreover, it proposes the constraint logic paradigm for the programming language of symbolic computation systems. First, it describes the integration of a separate constraint logic inference engine with the functional language of the symbolic computation system AlgBench. The procedural, functional, and APL-like programming styles are inherited from Mathematica and are integrated on top of its term-rewriting mechanism. The proposed language could serve as a stand alone programming language. Second, it shows the efficient compilation of the resulting language to an intermediate code. The compiler generates code for a uniform abstract...

110733. O(N³) Algorithm for Bisimulation Equivalence w.r.t CTL* without the Next-Time Operator between Kripke Structures - Mahesh Girkar,Robert Moll
Concurrent systems are often modeled by labeled state--transition graphs called Kripke Structures [5]. To reason about such systems, one standard approach is to provide a temporal semantic for the structure. Properties of interest regarding concurrency can then be expressed using a temporal logic formula. In this paper we consider the following problem: Given a Kripke structure, determine for all pairs of states s and s 0 whether they are equivalent with respect to CTL =X (i.e. s and s 0 model the same set of formulas in CTL =X). CTL [3], a new logic, incorporates the features of both Linear Temporal Logic and Branching Temporal Logic. In Logic CTL =X, the nexttime operator is discarded,...

110734. Automatic Symbolic Verification of Embedded Systems - Rajeev Alur,Thomas A. Henzinger,Pei-hsin Ho
. We present a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as Hybrid Automata---communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure, and temperature. The system requirements are specified in a temporal logic with stop watches, and verified by symbolic fixpoint computation. The verification procedure---implemented in the Cornell Hybrid Technology Tool, HyTech---applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded, and duration requirements of digital controllers, schedulers, and distributed algorithms. 1...

110735. On Constructive Negation for Disjunctive Logic Programs - Jorge Lobo
Answers for queries in logic programs, can be seen as formulas involving only equality and inequality predicates. This representation permits the extension of proofprocedures as SLDNF-resolution to handle non-ground negative queries. In this paper, we extend these ideas to the class of disjunctive logic programs. Keywords: Theory, Constructive Negation, Disjunctive programs. 1 Introduction Procedural interpretations for rules of negation in logic programming generally have been confined to ground literals [2, 19]. The restriction is imposed since answers for queries provided by these procedures are based solely on substitutions and most general unifiers. However, recently a new approach to the form of an answer, termed constructive negation [3], has permitted the extension...

110736. A Matrix Characterization for MELL - Christoph Kreitz
. We present a matrix characterization of logical validity in the multiplicative fragment of linear logic with exponentials. In the process we elaborate a methodology for proving matrix characterizations correct and complete. Our characterization provides a foundation for matrixbased proof search procedures for MELL as well as for procedures which translate machine-found proofs back into the usual sequent calculus. 1 Introduction Linear logic [12] has become known as a very expressive formalism for reasoning about action and change. During its rather rapid development linear logic has found applications in logic programming [14,19], modeling concurrent computation [11], planning [18], and other areas. Its expressiveness, however, results in a high complexity. Propositional linear...

110737. Neuronal Architectures for Pattern-theoretic Problems - David Mumford
this paper is the proposition that the computational analysis of vision -- and speech, tactile sensing, motor control, etc. -- (the theory of the computation as Marr called it (Marr, 82)) has is reaching a point where it can provide a clearer and deeper description of the essential tasks of vision as well as a wide range of other cognitive tasks. For instance, the development of algorithms for character recognition or for face recognition or for road tracking from a moving vehicle (three problems which have been much studied on account of their potential applications) forces the researcher to deal with noisy, complex real world data. In doing...

110738. Formal Reasoning about Actor Programs Using Temporal Logic - Susanne Schacht
We here present an approach to reasoning about actor programs on the basis of temporal logic. Temporal logic is particularly appropriate for the specification of concurrent programs, but most known temporal logic proof systems for concurrent computations rely on imperative language constructs, ignoring, e.g., the creation of processes and the dynamic configuration of communication channels, which are crucial for actor based programming. This work was supported by a grant from DFG under account Ha2097/1-3. 1 Temporal logic as a tool for specification and verification Temporal logic is particularly appropriate for reasoning about programs for which a corresponding statement in terms of their operational or denotational semantics is too...

110739. Sequent Calculus and the Specification of Computation - Lecture Notes - C Dale Miller
4 2 Overview and motivation 5 2.1 Roles for logic in the specific of computations . . . . . . . . . . . . . . . . . . 5 2.2 Desiderata for declarative programming . . . . . . . . . . . . . . . . . . . . . 6 2.3 Relating algorithm and logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3 A First-Order Logics 8 3.1 Types and signatures . ....

110740. Tabulated Resolution for Well Founded Semantics - Roland Bol,Lars Degerstedt
Based on the search forest for positive programs as defined by Bol and Degerstedt, we define a tabulated version of SLS-resolution that is sound and complete w.r.t. well founded semantics. In contrast to SLS-resolution as proposed by Przymusinski and by Ross, a positivistic computation rule is not required. This proposal is closely related to that of Chen and Warren, but it relies on tabulation for both positive and negative recursion. In this way, only one forest needs to be constructed, rather than a forest for each negative context. For function-free programs, the resulting search forest is finite. Keywords: logic programming, deductive databases, well founded semantics, tabulation, search forest, SLS-resolution, implementation. 1 Introduction It...

 

Busque un recurso