Wednesday, July 23, 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,800

110721. Minimal Logic Re-Synthesis For Engineering Change - Gitanjali Swamy,Sriram Rajamani,Chris Lennard,Robert K. Brayton
Introduction Logic synthesis refers to the process of optimizing a logic description of a circuit, given as a net-list of logic (boolean) gates [8]. This representation can be optimized for area(minimum), delay (minimum or meeting requirements), and power(minimum). Since these problems are hard to solve exactly, heuristic algorithms are generally used. However, these algorithms are unstable; if a small change is made in the network function, the output of the synthesis algorithm may vary greatly from the previous implementation. A designer can invest effort in optimizing the original design by hand, so it is desirable that most of the hand-designed or optimal parts be preserved, even when changes are made to...

110722. Compiler-Directed Early Load-Address Generation - Ben-chung Cheng,Daniel A. Connors,Wen-mei W. Hwu
Two orthogonal hardware techniques, table-based address prediction and early address calculation, for reducing the latency of load instructions have been recently proposed. The key idea behind both of these techniques is to speculatively perform loads early in the processor pipeline using predicted values for the loads' addresses. These techniques have required either a large hardware table or complex register bypass logic to be implemented in order to accurately predict the important loads in the presence of a large number of less-important loads. This paper proposes a compilerdirected approach that allows a streamlined version of both of these techniques to be effectively used together. The compiler provides directives to indicate which prediction mechanism to use...

110723. Empirical Evaluation of the CRAY-T3D: A Compiler Perspective - Remzi H. Arpaci,David E. Culler,Arvind Krishnamurthy,Steve G. Steinberg,Katherine Yelick
Most recent MPP systems employ a fast microprocessor surrounded by a shell of communication and synchronization logic. The CRAY-T3D 1 provides an elaborate shell to support global-memory access, prefetch, atomic operations, barriers, and block transfers. We provide a detailed empirical performance characterization of these primitives using micro-benchmarks and evaluate their utility in compiling for a parallel language. We have found that the raw performance of the machine is quite impressive and the most effective forms of communication are prefetch and write. Other shell provisions, such as the bulk transfer engine and the external Annex register set, are cumbersome and of...

110724. Programming and Interface Specification Language of JIVE - Specification and Design Rationale - Peter Muller,Jorg Meyer,Arnd Poetzsch-heffter,Fachbereich Informatik,Fernuniversitat Hagen
This report describes the programming and interface specification language of the Java Interactive Verification Environment Jive. The Jive system is a prototype implementation of a logic-based programming-environment for an object-oriented programming language. Logic-based programming-environments are language-dependent software development tools that support formal specification and verification. We summarize the properties of an ideal programming language for the prototype and argue that Java is a good candidate. The design of the supported Java subset is discussed and a formal definition of the abstract syntax is presented. Program specifications are denoted in an interface specification language. This report discusses the design of the Jive interface specification language and presents its abstract syntax. An...

110725. Contrary-to-Duty Obligations - Henry Prakken,Marek Sergot
We investigate under what conditions contrary-to-duty (CTD) structures lacking temporal and action elements can be given a coherent reading. We argue, contrary to some recent proposals, that CTD is not an instance of defeasible reasoning, and that methods of nonmonotonic logics are inadequate since they are unable to distinguish between defeasibility and violation of primary obligations. We propose a semantic framework based on the idea that primary and CTD obligations are obligations of different kinds: a CTD obligation pertains to, or pre-supposes, a certain context in which a primary obligation is already violated. This framework is presented initially as an extension of Standard Deontic Logic (SDL), a normal modal...

110726. Application Of Esop Minimization In Machine Learning And Knowledge Discovery - Marek A. Perkowski Tim Ross,Dave Gadd,Jeffrey A. Goldman,Ning Song
This paper presents a new application of an Exclusive-Sum-Of-Products (ESOP) minimizer EXORCISM-MV-2: to Machine Learning, and particularly, in Pattern Theory. An analysis of various logic synthesis programs has been conducted at Wright Laboratory for machine learning applications. Creating a robust and efficient Boolean minimizer for machine learning that would minimize a decomposed function cardinality (DFC) measure of functions would help to solve practical problems in application areas that are of interest to the Pattern Theory Group - especially those problems that require strongly unspecified multiple-valued-input functions with a large number of variables. For many functions, the complexity minimization of EXORCISM-MV-2 is better than that of Espresso. For small functions, they are worse than those of the...

110727. Fixpoint 3-Valued Semantics for Autoepistemic Logic - Marc Denecker,Victor Marek
The paper presents a constructive 3-valued semantics for autoepistemic logic (AEL). We introduce a derivation operator and define the semantics as its least fixpoint. The semantics is 3-valued in the sense that, for some formulas, the least fixpoint does not specify whether they are believed or not. We show that complete fixpoints of the derivation operator correspond to Moore's stable expansions. In the case of modal representations of logic programs our least fixpoint semantics expresses well-founded semantics or 3-valued Fitting-Kunen semantics (depending on the embedding used). We show that, computationally, our semantics is simpler than the semantics proposed by Moore (assuming that the polynomial hierarchy does not collapse). Introduction 1 We describe a 3-valued semantics for modal theories that...

110728. Permissive Subsorted Partial Logic in CASL - Maura Cerioli,Anne Haxthausen
. This paper presents a permissive subsorted partial logic used in the CoFI Algebraic Specification Language. In contrast to other ordersorted logics, subsorting is not modeled by set inclusions, but by injective embeddings allowing for more general models in which subtypes can have different data type representations. Furthermore, there are no restrictions like monotonicity, regularity or local filtration on signatures at all. Instead, the use of overloaded functions and predicates in formulae is required to be sufficiently disambiguated, such that all parses have the same semantics. An overload resolution algorithm is sketched. 1 Introduction During the past decades a large number of algebraic specification languages have been developed. The presence of...

110729. Ambiguity and the Principle of Idiosyncratic Interpretation - Kees Van Deemter
This paper discusses logics whose premisses and/or conclusions can contain ambiguous material. Two different kinds of applications are sketched for these logics. First, the paper discusses how logics with ambiguous expressions can shed light on the way in which human hearers or readers understand certain `paradoxical' logical arguments, in which crucial use is made of ambiguous material. Second, the paper uses practical (i.e., computational) applications to show how a logic of ambiguous expressions can be used to avoid interpretational deadlock in such systems. Here a key role is played by the Principle of Idiosyncratic Interpretation, which states that, in a given context of occurrence, different...

110730. A Uniform Framework for Concept Definitions in Description Logics - Maurizio Lenzerini
Most modern formalisms used in Databases and Artificial Intelligence for describing an application domain are based on the notions of class (or concept) and relationship among classes. One interesting feature of such formalisms is the possibility of defining a class, i.e., providing a set of properties that precisely characterize the instances of the class. Many recent articles point out that there are several ways of assigning a meaning to a class definition containing some sort of recursion. In this paper, we argue that, instead of choosing a single style of semantics, we achieve better results by adopting a formalism that allows for different semantics to coexist. We...

110731. Logic Programming with Constructor-based Type Constraints - Hans-joachim Goltz
A concept of types and type sorts for logic programming is introduced, where types and type sorts are regarded as constraints. Instead of defining "well-sorted" terms and substitutions, type constraints and type sort constraints are defined. The approach is based on term models. A type is interpreted as a set of object terms and a type sort is interpreted as a set of types. Parameters of types can be object variables, object terms, and type variables. Types are defined by means of type rules which can be regarded as rules for the generation of the elements belonging to the corresponding type. The definitions of types and...

110732. Correct-schema-guided Synthesis of Steadfast Programs - Pierre Flener,Kung-kiu Lau,Mario Ornaghi
It can be argued that for (semi-)automated software development, program schemas are indispensable, since they capture not only structured program design principles, but also domain knowledge, both of which are of crucial importance for hierarchical program synthesis. Most researchers represent schemas purely syntactically (as higher-order expressions) . This means that the knowledge captured by a schema is not formalised. We take a semantic approach and show that a schema can be formalised as an open (firstorder) logical theory that contains an open logic program. By using a special kind of correctness for open programs, called steadfastness, we can define and reason about the correctness of schemas. We also show how to use...

110733. A New Continuous Propositional Logic - Riccardo Poli,Mark Ryan,Aaron Sloman
In this paper we present Minimal Polynomial Logic (MPL), a generalisation of classical propositional logic which allows truth values in the continuous interval [0; 1] and in which propositions are represented by multi-variate polynomials with integer coefficients. The truth values in MPL are suited to represent the probability of an assertion being true, as in Nilsson's Probabilistic Logic, but can also be interpreted as the degree of truth of that assertion, as in Fuzzy Logic. However, unlike fuzzy logic MPL respects all logical equivalences, and unlike probabilistic logic it does not require explicit manipulation of possible worlds. In the paper we describe the derivation and the properties of this new form...

110734. Equational Reasoning with 2-dimensional Diagrams - Yves Lafont
The significance of the 2-dimensional calculus, which goes back to Penrose, has already been pointed out by Joyal and Street. Independently, Burroni has introduced a general notion of n-dimensional presentation and he has shown that the equational logic of terms is a special case of 2-dimensional calculus. Here, we propose a combinatorial definition of 2-dimensional diagrams and a simple method for proving that certain monoidal categories are finitely 2-presentable. In particular, we consider Burroni's presentation of finite maps and we extend it to the case of finite relations. This paper should serve as a reference for our future work on symbolic computation, including a theory of 2-dimensional rewriting...

110735. 1st Order Logic Formal Concept Analysis: from logic programming to theory - Vol Nr,Laurent Chaudron,Nicolas Maille
In this paper, we analyze and define the introduction of 1st order logic in Formal Concept Analysis (FCA); the aims are both theoretical (as a complete model is needed) and applied (so as to improve expression power of FCA as a knowledge mining tool and the relevance of its results). Our contribution consists in: i) the implementation of classical FCA in logic programming and the analysis of real cases, ii) the design of a complete 1st order FCA model, iii) the implementation of this 1st order FCA. Keywords: Formal Concept Analysis, Knowledge Representation, Concepts Discovery, Rule induction, Logic Programming. Authors' affiliation and address: Onera Cert 2 avenue Edouard Belin BP 4025 F-31055 Toulouse Cedex 04...

110736. A Linear Logic View of Gamma Style Computations as Proof Searches - Paola Bruscoli,Alessio Guglielmi
Using the methodology of abstract logic programming in linear logic, we establish a correct and complete translation between the language Nabla and first order linear logic. Nabla is a modification of the coordination language Gamma with parallel and sequential composition. Nabla, without modifying Gamma basic computational model, is amenable to this kind of analysis, at the price of a weaker expressive power. The translation is correct and complete in the sense that we establish a two way correspondence between computations in Nabla and the search for proofs in a suitable fragment of first order linear logic. Moreover, the translation is not an encoding, meaning that to the algebraic structure...

110737. A Theory of Nonmonotonic Inheritance Based on Annotated Logic - Krishnaprasad Thirunarayan,Michael Kifer
We propose a logical language for representing networks with nonmonotonic multiple inheritance. The language is based on a variant of annotated logic studied in [5, 6, 17, 18, 19, 20, 21]. The use of annotated logic provides a rich setting that allows to disambiguate networks whose topology does not provide enough information to decide how properties are to be inherited. The proposed formalism handles inheritance via strict as well as defeasible links. We provide a formal account of the language, describe its semantics, and show how a unique intended model can be associated with every inheritance specification written in the language. Finally, we present an algorithm that correctly...

110738. Tunable Formalism In Object-Oriented Systems Analysis: Meeting The Needs Of Both Theoreticians And Practitioners - Stephen W. Clyde,David W. Embley,Scott N. Woodfield
+ This work has been partially supported by HewlettPackard through graduate fellowships and equipment grants. Object-oriented Systems Analysis (OSA) [7] meets the needs of both theoreticians and practitioners by providing tunable formalism. In this paper, we show how an OSA user's use of formalism can be tuned from completely informal to completely formal. We give OSA's underlying formal definition that makes this possible as a two-step process involving a temporal, first-order logic language, and a mathematical interpretation. We also show how the formal definition provides answers to fundamental, practical questions related to object-oriented software development. Finally, we show how OSA allows varying levels of abstraction and completion so that engineers, tool builders, and researchers can tune the formalism to suit...

110739. Desiderata for Interactive Verification Systems DRAFT - Konrad Slind,Christian Prehofer
What facilities should an interactive verification system provide? We take the pragmatic view that the particular logic underlying a proof system is not as important as the support that is provided. Although a plethora of logics have been implemented, we think that there is a common kernel of support that a proof system ought to provide. Towards this end, we give detailed suggestions for verification support in three major areas: formalization, proof, and interface. Although our perspective comes from experience with highly expressive logics such as set theory, higher order logic, and type theory, we think our analyses apply more generally. Introduction Currently, theorem provers are used in the...

110740. Logic Is Not Enough: Why Reasoning About Another Person's Beliefs Is Reasoning Under Uncertainty - Anthony Jameson
A system that reasons about the beliefs of a person must in general be able to ascribe a good deal of general background knowledge to that person, often in the absence of reliable evidence that the person possesses that knowledge. In some cases it is possible to make the necessary inferences within a logical framework, often as default inferences, using as premises information about the person's membership in some group or information about the system's own knowledge. But these approaches do not in general adequately deal with the uncertainty that pervades the ascription of general background knowledge. An explicitly probabilistic framework, intuitive psychometrics, was developed to provide a...

 

Busque un recurso