Monday, July 28, 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,821

110721. On Nominal Delay Minimization in LUT-Based FPGA Technology Mapping - Jason Cong,Yuzheng Ding
We study the nominal delay minimization problem in LUTbased FPGA technology mapping, where interconnect delay is assumed proportional to net fanout size. We prove that the delay-optimal K-LUT mapping problem under the nominal delay model is NP-hard when K 3, and remains NP-hard for duplication-free mapping and tree-based mapping for K 5 (but is polynomial time solvable for K = 2). We also present a simple heuristic to take nominal delay into consideration during LUT mapping for delay minimization. 1 Introduction Lookup-table (LUT) based FPGA [8, 10] is a popular architecture in which the basic programmable logic block is a K-input lookup-table (K-LUT), built in SRAM, which can implement any Boolean function of...

110722. Automatic Verification of Transactions on an Object-Oriented Database - David Spelt,Herman Balsters
. In the context of the object-oriented data model, a compiletime approach is given that provides for a significant reduction of the amount of run-time transaction overhead due to integrity constraint checking. The higher-order logic Isabelle theorem prover is used to automatically prove which constraints might, or might not be violated by a given transaction in a manner analogous to the one used by Sheard and Stemple (1989) for the relational data model. A prototype transaction verification tool has been implemented, which automates the semantic mappings and generates proof goals for Isabelle. Test results are discussed to illustrate the effectiveness of our approach. Keywords: object-oriented databases, transaction semantics, transaction verification 1 Introduction Static...

110723. Guarded Evaluation: Pushing Power Management to Logic Synthesis/Design - Vivek Tiwari,Sharad Malik,Pranav Ashar
The need to reduce the power consumption of the next generation of digital systems is clearly recognized. At the system level, power management is a very powerful technique and delivers large and unambiguous savings. This paper describes the development and application of algorithms that use ideas similar to power management, but that are applicable to logic level synthesis/design. The proposed approach is termed guarded evaluation. The main idea here is to determine, on a per clock cycle basis, which parts of a circuit are computing results that will be used, and which are not. The sections that are not needed are then "shut off", thus saving the power used in all the...

110724. Bisimulation, Model Checking and Other Games - Colin Stirling
Contents 1 Introduction 2 2 Process Calculi 2 3 Equivalences, Modal and Temporal Logics 6 3.1 Interactive games and bisimulations . . . . . . . . . . . . . . . 8 3.2 Modal logic and bisimulations . . . . . . . . . . . . . . . . . . . 13 3.3 Temporal properties and modal mu-calculus . . . . . . . . . . 15 3.4 Second-order propositional modal logic . . . . . . . . . . . . . . 21 4 Property Checking and Games 22 4.1 Subformulas and subsumption ....

110725. Extending Temporal Actiom Logic for Ramification and Concurrency - Joakim Gustafsson Link
An autonomous agent operating in a dynamical environment must be able to perform several "intelligent" tasks, such as learning about the environment, planning its actions and reasoning about the effects of the choosen actions. For this purpose, it is vital that the agent has a coherent, expressive, and well understood way to represent its knowledge about the world. The research field "Logics of Action and Change" is concerned with using logics for modeling agents and their interaction with dynamical, changing environments. In this thesis we extend an existing logic of action and change, TAL, to handle ramification and concurrency. Historically all knowledge about the dynamics of the modeled world has been...

110726. Generalized Notions of Mind Change Complexity - Arun Sharma,Frank Stephan,Yuri Ventsov
Speed of convergence in Gold's identification in the limit model can be measured by deriving bounds on the number of mind changes made by a learner before the onset of convergence. Two approaches to date are bounds given by constants (referred here as Type 1) and bounds expressed as constructive ordinals (referred as Type 2). The use of ordinals has recently been successfully employed to measure the mind change complexity of learning rich concept classes such as unions of pattern languages, elementary formal systems and logic programs. Motivated by these applications, the present work introduces two more general approaches to bounding mind changes. These are based on counting by going down in a...

110727. On the Declarative and Procedural Semantics of Logic Programs - Teodor C. Przymusinski
One of the most important and difficult problems in logic programming is the problem of finding a suitable declarative or intended semantics for logic programs. The importance of this problem stems from the declarative character of logic programming, whereas its difficulty can be largely attributed to the non-monotonic character of the negation operator used in logic programs. The problem can therefore be viewed as the problem of finding a suitable formalization of the type of non-monotonic reasoning used in logic programming. In this paper we introduce a semantics of logic programs based on the class PERF(P) of all, not necessarily Herbrand, perfect models of a program P and...

110728. Subsumption for Semantic Query Optimization in OODB - Domenico Beneventano,Sonia Bergamaschi,Claudio Sartori
The purpose of semantic query optimization is to use semantic knowledge (e.g. integrity constraints) for transforming a query into an equivalent one that may be answered more efficiently than the original version. This paper proposes a general method for semantic query optimization in the framework of OODBs (Object Oriented Database Systems). The method is applicable to the class of conjunctive queries and is based on two ingredients: a description logic able to express both class descriptions and integrity constraints rules (IC rules) as types; subsumption computation between types to evaluate the logical implications expressed by IC rules. 1 Introduction In database environment, semantic knowledge is usually expressed in terms of...

110729. Modeling a Hardware Synthesis Methodology in Isabelle - David Basin,Stefan Friedrich
. Formal Synthesis is a methodology developed at Kent for combining circuit design and verification. We have reinterpreted this methodology in Isabelle's theory of higher-order logic so that circuits are synthesized using higher-order resolution. Our interpretation simplifies and extends Formal Synthesis both conceptually and in implementation. It also supports integration of this development style with other synthesis methodologies and leads to techniques for developing new classes of circuits, e.g., recursive descriptions of parameterized circuits. 1 Introduction Verification by formal proof is time intensive and this is a burden in bringing formal methods into software and hardware design. One approach to reducing the verification burden is to combine development and verification by...

110730. Factored Edge-Valued Binary Decision Diagrams - Paul Tafertshofer,Massoud Pedram
Factored Edge-Valued Binary Decision Diagrams form an extension to Edge-Valued Binary Decision Diagrams. By associating both an additive and a multiplicative weight with the edges, FEVBDDs can be used to represent a wider range of functions concisely. As a result, the computational complexity for certain operations can be significantly reduced compared to EVBDDs. Additionally, the introduction of multiplicative edge weights allows us to directly represent the so-called complement edges which are used in OBDDs, thus providing a one to one mapping of all OBDDs to FEVBDDs. Applications such as integer linear programming and logic verification that have been proposed for EVBDDs also benefit from the extension. We...

110731. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp - Matt Kaufmann,J Strother Moore
ACL2 is a re-implemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. This paper deals primarily with how we scaled up Nqthm's logic to an "industrial strength" programming language --- namely, a large applicative subset of Common Lisp --- while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of ACL2 and we briefly summarize two industrial applications: a model of the Motorola CAP digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on...

110732. Paralleltermgraphrewritingand Concurrent Logic Programs - G. A. Papadopoulos
General term graph rewriting is a powerful computational model, suitable for implementing a wide variety of declarative language paradigms. Here, we address the problems involved in the implementation, on a loosely-coupled architecture, of an intermediate language based on term graph rewriting, DACTL. In general, such problems are severe, so a subset of this language called MONSTR is defined, free from some of the inefficiencies in the original model (such as an excessive necessity for locking). Superficially, much of the expressiveness of the original model is compromised thereby, especially with regard to the implementation of concurrent logic languages. However, transformation techniques that are valid in the context of declarative...

110733. From Sound and Complete to Approximate Deduction - Fabio Massacci
. The computational complexity of reasoning in classical and non-classical logics makes traditional deduction not feasible in practice. This paper advocates the introduction of approximate proofs within automated deduction for classical and non-classical logics and a corresponding intuition of superficial semantics to overcome this limitation. Recent and past years have seen a vigorous development of automated deduction procedures for classical and non-classical logics. Calculi for logics for knowledge and belief, actions and programs, concurrency and temporal reasoning, description logics for knowledge representation have been developed (e.g. see [2, 3, 6, 7, 10, 11]) and corresponding systems implemented. Classical logic has gone far beyond and competitions between provers are...

110734. Disjunctive Defaults - Michael Gelfond,Vladimir Lifschitz
A generalization of Reiter's default logic is proposed that provides an improved treatment of default reasoning with disjunctive information. The new system --- the disjunctive default logic --- is used in the paper to reexamine the "broken-hand" example of Poole. We also compare the expressive power of this approach with two other approaches which interpret disjunctive information within the standard default logic. Finally, we show that our semantics of disjunctive default logic is a generalization of the semantics of disjunctive and extended disjunctive databases. 1 INTRODUCTION In this paper we generalize the theory of default reasoning developed by Reiter [Rei80]. The generalization is motivated by a difficulty encountered in attempts to use defaults in the presence of...

110735. A Logical Characterization of Bisimulation for Labeled Markov Processes - Abbas Edalat,Prakash Panangaden
This paper gives a logical characterization of probabilistic bisimulation for Markov processes introduced in [BDEP97]. The thrust of that work was an extension of the notion of bisimulation to systems with continuous state spaces; for example for systems where the state space is the real numbers. In the present paper we study the logical characterization of probabilistic bisimulation for such general systems. This study revealed some unexpected results even for discrete probabilistic systems. ffl Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition. ffl Bisimulation can be characterized by several inequivalent...

110736. Induction of First-Order Decision Lists: Results on Learning the Past Tense of English Verbs - Raymond J. Mooney,Mary Elaine Califf
This paper presents a method for inducing logic programs from examples that learns a new class of concepts called first-order decision lists, defined as ordered lists of clauses each ending in a cut. The method, called Foidl, is based on Foil (Quinlan, 1990) but employs intensional background knowledge and avoids the need for explicit negative examples. It is particularly useful for problems that involve rules with specific exceptions, such as learning the past-tense of English verbs, a task widely studied in the context of the symbolic/connectionist debate. Foidl is able to learn concise, accurate programs for this problem from significantly fewer examples than previous methods (both connectionist...

110737. Reinforcement Learning of Hierarchical Fuzzy Behaviors for Autonomous Agents - Andrea Bonarini,Proyecto Sur Ediciones
Reinforcement learning is a suitable approach to learn behaviors for Autonomous Agents, but it is usually too slow to be applied in real time on embodied agents [8]. In this paper, we present the results that we have obtained by adopting a careful design of the control architecture and of the learning sessions, aimed at reducing the learning computation. The agent learns in simplified environments one or more basic behaviors, then it learns how to put them together, and, finally, it adapts the behaviors previously learnt, running in the operating environment. This makes it possible to cut the computational effort to learn the control system. Moreover, this approach produces in simulation a first behavior that enables the...

110738. Performance Prediction for the HTMT: A Programming Example - Jose Nelson Amaral,Guang R. Gao,Phillip Merkey,Thomas Sterling,Zachary Ruiz,Sean Ryan
This paper presents an analytical performance prediction for the implementation of Cannon's matrix multiply algorithm in the Hybrid Technology Multi-Threading (HTMT) architecture [8]. The HTMT subsystems are built from new technologies: super-conducting processor elements (called SPELLs [5]), a network based on RSFQ (Rapid Single Flux Quantum) logic devices (called

110739. Oracle Semantics for Prolog - Roberto Barbuti,Michael Codish,Roberto Giacobazzi,Michael Maher
This paper proposes to specify semantic definitions for logic programming languages such as Prolog in terms of an oracle which specifies the control strategy and identifies which clauses are to be applied to resolve a given goal. The approach is quite general. It is applicable to Prolog to specify both operational and declarative semantics as well as other logic programming languages. Previous semantic definitions for Prolog typically encode the sequential depth-first search of the language into various mathematical frameworks. Such semantics mimic a Prolog interpreter in the sense that following the "leftmost" infinite path in the computation tree excludes computation to the right of this path from being...

110740. Generalized Search Trees for Database Systems
) Joseph M. Hellerstein University of Wisconsin, Madison jmh@cs.berkeley.edu Jeffrey F. Naughton University of Wisconsin, Madison naughton@cs.wisc.edu Avi Pfeffer University of California, Berkeley avi@cs.berkeley.edu Abstract This paper introduces the Generalized Search Tree (GiST), an index structure supporting an extensible set of queries and data types. The GiST allows new data types to be indexed in a manner supporting queries natural to the types; this is in contrast to previous work on tree extensibility which only supported the traditional set of equality and range predicates. In a single data structure, the GiST provides all the basic search tree logic required by a database system, thereby unifying disparate structures such as B+-trees and R-trees in a single piece of code, and...

 

Busque un recurso