Sunday, February 1, 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 139,687

110721. Acceptable Programs Revisited - Pascal Hitzler,Anthony Karel Seda
Acceptable logic programs have been studied extensively in the context of proving termination of Prolog programs. It is difficult, however, to establish acceptability from the definition since this depends on finding a suitable model, which need not be a Herbrand model in general, together with a suitable level mapping that one can use to check the conditions which characterize acceptability. In this paper, we will see that when working over a fixed but arbitrary preinterpretation, a method can be provided for obtaining both a suitable model and a canonical level mapping which are sufficient for this purpose. Furthermore, the canonical model and level mapping obtained will turn out...

110722. A Semantic Model of Types and Machine Instructions for Proof-Carrying Code - Amy P. Felty
Proof-carrying code is a framework for proving the safety of machine-language programs with a machinecheckable proof. Such proofs have previously defined type-checking rules as part of the logic. We show a universal type framework for proof-carrying code that will allow a code producer to choose a programming language, prove the type rules for that language as lemmas in higher-order logic, then use those lemmas to prove the safety of a particular program. We show how to handle traversal, allocation, and initialization of values in a wide variety of types, including functions, records, unions, existentials, and covariant recursive types.

110723. The Design and Evaluation of an Asynchronous Microprocessor - S. B. Furber,P. Day,J. D. Garside,N. C. Paver,S. Temple,J. V. Woods
AMULET1 is a fully asynchronous implementation of the ARM microprocessor which was designed at Manchester University between 1991 and 1993. First silicon arrived in April 1994 and was found to be functional, demonstrating that asynchronous design of complex circuits is feasible with present day CAD tools. This paper presents the motivation for the work, some of the design choices which were made, the problems which were encountered during the development of the design and the characteristics of the device itself. The future potential for asynchronous circuits is also discussed. 1: Introduction The growth in demand for high performance portable computing...

110724. Justus-Liebiguniversit - Research Report,Thomas Eiter,Georg Gottlob,Yuri Gurevich
. Existential second-order logic (ESO) and monadic second-order logic (MSO) have attracted much interest in logic and computer science. ESO is a much more expressive logic over word structures than MSO. However, little was known about the relationship between MSO and syntactic fragments of ESO. We shed light on this issue by completely characterizing this relationship for the prefix classes of ESO over strings, (i.e., finite word structures). Moreover, we determine the complexity of model checking over strings, for all ESO-prefix classes. Let ESO(Q) denote the prefix class containing all sentences of the shape 9RQ' where R is a list of predicate variables, Q is a first-order...

110725. What Is A Skeptical Proof? - Michael Thielscher
. We investigate the task of skeptically reasoning in extensionbased, nonmonotonic logics by concentrating on general argumentation theories. The restricted applicability of Dung's notion of skeptical provability in his well-known argumentation framework is illustrated, and a new approach based on the notion of a claim associated with each argument is proposed. We provide a formal definition of a skeptical proof in our framework. As a concrete formalism, default logic in case of normal default theories is embedded in the general framework. We prove a formal correspondence between the two notions of skeptical provability, which enables us to adopt the general concept of a skeptical proof into default logic. 1 Introduction This paper...

110726. clp(B): Combining Simplicity and Efficiency in Boolean Constraint Solving - Daniel Diaz
. We present the design and the implementation of clp(B): a boolean constraint solver in the Constraint Logic Programming paradigm. This solver is based on local propagation methods and follows the "glassbox " approach of compiling high-level constraints into primitive low-level ones. We detail its integration into the WAM showing that the necessary extension is truly minimal since only four new instructions are added. The resulting solver is around an order of magnitude faster than other existing boolean solvers. 1 Introduction Constraint Logic Programming (CLP) combines both the declarativity of Logic Programming and the ability to reason and compute with partial information (constraints) on specific domains, thus opening up a wide...

110727. Quantitative Disjunctive Logic Programming: Semantics and Computation - Cristinel Mateis
this paper are given in Appendix B.

110728. Type Inference with Constrained Types - Martin Odersky,Martin Wehr
this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints, analogous to the CLP(X) framework in constraint logic programming [JM94]. Particular type systems can be obtained by instantiating the parameter X to a specific constraint system. The Hindley /Milner system itself is obtained by instantiating X to the standard Herbrand constraint system.

110729. Handling Preferences in Negotiation Dialogue Frames - Aspassia Daskalopulu,Chris Reed
. Complex argumentation-based interaction can be characterised by a rich model of inter-agent communication based upon the construct of a dialogue frame. This approach is shown to have computational benefits and can be easily extended to include models of agents' preferences. The process of negotiation is founded upon the notion of compromise and this comes about as a result of agents' preferences: an agent may be willing to make concessions if in so doing, preferred states of affairs obtain. This paper explores a formal approach to representing such preference criteria, and the means by which evaluation of potential contracts can be carried out. The resulting system supports sophisticated...

110730. rd. International Conference on Fuzzy Logic, Neural Nets and Soft Computing (IIZUKA'94), pp. 651-652, Iizuka - Japan, August 1-7, 1994. - C. J. Jimnez,A. Barriga,S. Snchez Solano
.-- A classification of inference systems based on approximate reasoning techniques is proposed. An alternative realization method is described for the particular SISC case, which enables reducing the silicon area and increasing the operation speed, making it especially appropriate for real time control applications. I. INTRODUCTION Fuzzy logic provides a conceptual and mathematical frame for those problems where the imprecise definition of variables and vague resolution strategies applied require the use of approximate reasoning techniques. This has led to the development of new processing structures which allow hardware implementations of fuzzy inference mechanisms [1]. Distinct taxonomies can be established for fuzzy inference systems according to different criteria. However, in order to compare their hardware realizations, it is...

110731. How to Normalize the Jay - Dieter Probst,Thomas Studer
In this note we give an elementary proof of the strong normalization property of the J combinator in combinatory logic by providing an explicit bound for the maximal length of the reduction path of a term. 1 Introduction The combinators I and J with their reduction rules Ia#a and Jabcd#ab(adc) were introduced by Rosser [2] in 1935. These two combinators are of particular interest since together they form a basis for the #I-calculus (cf. e.g. Barendregt [1]). In combinatory logic, it is natural to ask whether a certain system is strongly normalizing, i.e. whether there does not exist a term with an infinite reduction path. Most standard combinators such...

110732. Goals, Desires, Utilities and Preferences - Leendert W. N,Torre E. Weydert
. In this paper we study the logic of goals, which are formalized as desires with an utilitarian semantics. In our framework goals have a dual character, because they are constraints on utility functions as well as constructors of these utility functions. The non-monotonic reasoning related to the constructors reflects that goals are used as heuristic approximations of preferences in decision making and planning. Moreover, our framework is based on bipolar additive preferences, where bipolarity means that goals can either result in a gain of utility if achieved, or a loss of utility if not achieved. The framework is used to illustrate different types of contextdependence and conflicts of goals. 1 Introduction Decision...

110733. 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...

110734. A Semantics for Evaluation Logic (Extended Version) - Eugenio Moggi
This paper proposes an internal semantics for the modalities and evaluation predicate of Pitts' Evaluation Logic, and introduces several predicate calculi (ranging from Horn sequents to Higher Order Logic), which are sound and complete w.r.t. natural classes of models. It is shown (by examples) that many computational monads satisfy the additional properties required by the proposed semantics. Introduction Evaluation logic EL T is a typed predicate logic (see [CP92, Pit91]) based on the metalanguage for computational monads ML T (a typed calculus introduced in [Mog91]), which permits statements about the evaluation of programs to values by the use of evaluation modalities. In particular, EL T might be used...

110735. Logic Program Transformation through Generalization Schemata - Pierre Flener,Yves Deville
In program synthesis, program transformation can be done on the fly, based on information generated and exploited during the program construction process. For instance, some logic program generalization techniques can be pre-compiled at the logic program schema level, yielding transformation schemata that give rise to elimination of the eureka discovery, full automation of the transformation process itself, and even the prediction whether and which optimizations will be achieved. 1 Introduction Programs can be classified according to their construction methodologies, such as divide-and-conquer, generate -and-test, top-down decomposition, global search, and so on, or any composition thereof. Informally, a program schema is a template program with a fixed control and...

110736. Plugging Data Constructs into Paradigm-Specific Languages: towards an Application to UML - Egidio Astesiano,Maura Cerioli,Gianna Reggio
. We are interested in the composition of languages, in particular a data description language and a paradigm-specific language, from a pragmatic point of view. Roughly speaking our goal is the description of languages in a component-based style, focussing on the data definition component. The proposed approach is to substitute the constructs dealing with data from the "data" language for the constructs describing data that are not specific to the particular paradigm of the "paradigm-specific" language in a way that syntax, semantics as well as methodologies of the two components are preserved. We illustrate our proposal on a toy example: using the algebraic specification language Casl, as data language, and...

110737. Coalgebras and Modal Logic - Martin Roiger
Coalgebras are of growing importance in theoretical computer science. To develop languages for them is significant for the specification and verification of systems modelled with them. Modal logic has proved to be suitable for this purpose. So far, most approaches have presented a language to describe only deterministic coalgebras. The present paper introduces a generalization that also covers non-deterministic systems. As a special case, we obtain the "usual" modal logic for Kripke-structures. Models for our modal language L F are F-coalgebras where the functor F is inductively constructed from constant sets and the identity functor using product, coproduct, exponentiation, and the power set functor. We define a language L F and show that it embeds into L F ....

110738. Modularity in Lambda Calculus - Antonino Salibra
The variety (equational class) of lambda abstraction algebras was introduced to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order predicate logic. In this paper a proof is given that the variety of lambda abstraction algebras is not congruence modular. Some simple applications of this result to lambda calculus are also obtained.

110739. Context Adaptation in Fuzzy Processing - Ricardo R. Gudwin,Fernando A. C. Gomide
: This paper deals with the influence of the context in fuzzy rule base systems. The linguistic variable definition of Zadeh is modified to permit context adaptation, and inference procedure is modified to handle context adaptation when evaluating fuzzy concepts. Procedures to determine context in different situations are provided. Context determination may be viewed as a kind of learning. An application example concerning supervisory control of group of elevators is also considered. I. Introduction A linguistic variable is a variable that assigns as its values linguistic labels, which are mapped onto the real world by a fuzzy set. A great problem which comprises this definition is the difficulty to fine tune membership functions, which is actually one of...

110740. Executable Temporal Logic for Distributed A.I. - Michael Fisher,Michael Wooldridge
This paper describes Concurrent METATEM, a programming language based on temporal logic, and applies it to the study of Distributed Artificial Intelligence (DAI). A Concurrent METATEM system consists of a number of asynchronously executing objects, which are able to communicate through broadcast message-passing. Each individual object directly executes a specification of its desired behaviour. Such specifications are given using a set of temporal logic `rules', determining how the object may generate `commitments', which it subsequently attempts to satisfy. This language provides a novel and powerful approach to representing DAI systems, where individual `agents' are specified in a natural way using temporal logic, while groups of agents communicate by...

 

Busque un recurso