Saturday, April 18, 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 145,267

110721. Digital Systems Design Using Constraint Logic Programming - Radoslaw Szymanek,Flavius Gruian,Krzysztof Kuchcinski
. This paper presents an application of finite domain constraint logic programming methods to digital system synthesis problems. The modeling methods address basic synthesis problems of high-level synthesis and system-level synthesis. Based on the presented models, the synthesis algorithms are then defined. These algorithms aim to optimize digital systems with respect to cost, power consumption, and execution time. Keywords. digital systems design, constraint logic programming 1. Introduction Recently, the system-on-chip concept has been proposed which is integration of many different system parts on a single chip. Current developments in the VLSI technology make it possible to build complex systems consisting of millions of components thus there is the potential...

110722. Leading--One Prediction With Concurrent Position Correction - J. D. Bruguera,T. Lang
This paper describes the design of a leading--one prediction (LOP) logic for floating--point addition with an exact determination of the shift amount for normalization of the adder result. Leading--one prediction is a technique to calculate the number of leading zeros of the result in parallel with the addition. However, the prediction might be in error by one bit, and previous schemes to correct this error result in a delay increase. The design presented here incorporates a concurrent position correction logic, operating in parallel with the LOP, to detect the presence of that error and produce the correct shift amount. We describe the error detection as part of the...

110723. Bayesian Logic Programs - Kristian Kersting,Luc De Raedt
Various proposals for combining first order logic with Bayesian nets exist. Many of these are based on the so-called knowledge-based model construction method, e.g. probabilistic logic programs by Ngo and Haddawy, relational Bayesian nets by Jaeger and the more recent probabilistic relational models by Koller et. al. Upon a first investigation these frameworks seem different despite the fact that they attack essentially the same problem. The relationship among these approaches has so far not been studied. The main contribution of this paper is, that we clarify the relation among the three existing frameworks. This is achieved through the introduction of...

110724. Annotated Constraint Logic Programming Applied to Temporal Reasoning - Thom Fruhwirth
Annotated constraint logic programming (ACLP) combines constraint logic programming (CLP) and generalized annotated programming (GAP). With ACL we propose a first order logic with constraints where formulas can be annotated. ACL comes with inference rules for annotated formulas and a constraint theory for handling annotations. We describe an implementation based on the standard interpreter for logic programs. The inference rules of ACL are turned into clauses of the interpreter, and the constraints on annotations are solved by a suitable constraint solver. Then we optimize the interpreter. We also introduce an instance of ACLP for reasoning about time. Temporal ACLP is conceptually simple while covering substantial parts of temporal...

110725. Recovering Sequentiality in Functional-Logic Programs - Juan Jos'e Moreno-navarro
. Efficient code generation in implementations of functional logic languages relies on the sequentiality of the program rules --- existence of an optimal evaluation order for arguments. Parallel evaluation of arguments in the presence of free variables is out of the question due to the possibility of backtracking and sharing of these variables among different arguments. In this paper we show that the lack of sequentiality is often syntactic rather than semantic and that a clever use of type information and strictness analysis can enable a compiler to generate sequential code from most programs. Keywords: Sequentiality, Abstract Interpretation, Functional Logic Programming. 1 Introduction The relationship between sequential term rewriting...

110726. Quantitative Comparison between Trajectory Estimates Obtained from a Binocular Camera Setup within a Moving Road Vehicle and from the Outside by a Stationary Monocular Camera - H. -h. Nagel,F. Heimes,S. Noltemeier,M. Haag
The image sequence evaluation system Xtrack detects, initializes, and tracks images of moving road vehicles in videosequences recorded at innercity tra#c scenes by a stationary camera. It recently has been supplemented, moreover, by subsystems which associate the geometric tracking results to conceptual representations of tra#c situations at innercityintersections. Such conceptual representations can be exploited byaFuzzy Metric-Temporal Logic subsystem in order to prepare a suitable conceptual description. A subsequent subsystem transforms this conceptual description into a natural language description of temporal developments in the recorded tra#c scenes. Weintend to study such an approach as a component of a driver assistance system to be installed within a road vehicle. As a #rst step, we establish a link...

110727. Logical Deduction using the Local Computation Framework - Nic Wilson,Gipsy Lane,Universite Paul Sabatier
The Local Computation Framework has been used to improve the efficiency of computation in various uncertainty formalisms. This paper shows how it can be applied to logical deduction in first-order logic, modal and conditional logics, circumscription and possibilistic logic. Keywords: Deduction, Theorem Proving, Local Computation, Possibilistic Logic, Modal and Conditional Logics, Circumscription 1 Introduction Computation in a number of uncertainty formalisms has recently been revolutionized by the notion of local computation. [22] and [13] showed how Bayesian probability could be efficiently propagated in a network of variables; this has already lead to sizeable successful applications, as well as a large body of literature on these Bayesian networks and related issues (e.g.,...

110728. How to Incorporate Negation in a Prolog Compiler
. Knowledge representation based applications require a more complete set of capabilities than those offered by conventional Prolog compilers. Negation is, probably, the most important one. The inclusion of negation among the logical facilities of LP has been a very active area of research, and several techniques have been proposed. However, the negation capabilities accepted by current Prolog compilers are very limited. In this paper, we discuss the possibility to incorporate some of these techniques in a Prolog compiler in an efficient way. Our idea is to mix some of the existing proposals guided by the information provided by a global analysis of the source code. Keywords: Semantics of Negation,...

110729. Operations on Proofs That Can Be Specified By Means of Modal Logic - Sergei N. Artemov
Explicit modal logic was first sketched by Godel in [16] as the logic with the atoms "t is a proof of F". The complete axiomatization of the Logic of Proofs LP was found in [4] (see also [6],[7],[18]). In this paper we establish a sort of a functional completeness property of proof polynomials which constitute the system of proof terms in LP. Proof polynomials are built from variables and constants by three operations on proofs: "Delta" (application), "!" (proof checker), and "+" (choice). Here constants stand for canonical proofs of "simple facts", namely instances of propositional axioms and axioms of LP in a given proof system. We...

110730. Adding Type Classes to Functional-logic Languages - Angel Herranz-nieva
: The paper discusses the advantages of introducing type classes into functionallogic languages. Type classes are a powerful type system included in the functional language Haskell that allow to model some of the object oriented programming features. A number of problems arise when type classes are combined with the functional and logic characteristics of the language, and we sketch some solutions. On the other hand it has a number of advantages like the declarative model of Prolog attribute variables or the integration in the language of bounded quantifiers. 1 Motivation During the last decade, several proposals have been made to achieve the combination of the most important declarative programming...

110731. Hybrid Probabilistic Programs: Algorithms and Complexity - Michael I. Dekhtyar,Alex Dekhtyar,V. S. Subrahmanian
Hybrid Probabilistic Programs (HPPs) are logic programs that allow the programmer to explicitly encode his knowledge of the dependencies between events being described in the program. In this paper, we classify HPPs into three classes called HPP1 ; HPP2 and HPPr ; r 3. For these classes, we provide three types of results for HPPs. First, we develop algorithms to compute the set of all ground consequences of an HPP. Then we provide algorithms and complexity results for the problems of entailment ("Given an HPP P and a query Q as input, is Q a logical consequenceof P ?") and consistency("Given an HPPP as input,...

110732. Specification of Real-Time and Hybrid Systems in Rewriting Logic - Peter Csaba
This paper explores the application of rewriting logic to the executable formal modeling of real-time and hybrid systems. We give general techniques by which such systems can be specified as ordinary rewrite theories, and show that a wide range of real-time and hybrid system models, including object-oriented systems, timed automata [3], hybrid automata [2], timed and phase transition systems [25], and timed extensions of Petri nets [1,35], can indeed be expressed in rewriting logic quite naturally and directly. Since rewriting logic is executable and is supported by several language implementations, our approach complements property-oriented methods and tools less well suited...

110733. Deliberative Stock Market Agents using Jinni and Defeasible Logic Programming - Paul Tarau
. Working with stock markets requires constant monitoring of the stock information which keeps changing continously, and the ability to take decisions instantaneously based on certain rules as the changes occur. In this paper, a framework for implementing a Deliberative MultiAgent System is developed. This system can be used as a proactive tool for expressing and putting to work high level stock trading strategies. In this framework, agents are able to monitor and extract stock market information via the World Wide Web and, using the domain knowledge provided in the form of defeasible rules, can reason in order to achieve the established goals. The overall system is integrated using Jinni...

110734. Verifiable Properties of Database Transactions - Michael Benedikt,Timothy Griffin,Leonid Libkin
It is often necessary to ensure that database transactions preserve integrity constraints that specify valid database states. While it is possible to monitor for violations of constraints at runtime, rolling back transactions when violations are detected, it is preferable to verify correctness statically, before transactions are executed. This can be accomplished if we can verify transaction safety with respect to a set of constraints by means of calculating weakest preconditions. We study properties of weakest preconditions for a number of transaction and specification languages. We show that some simple transactions do not admit weakest preconditions over first-order logic and some of its extensions such as first-order logic...

110735. Reconfigurable Architectures and General-Purpose Computing in the MOS VLSI Era - Andr E Dehon
The hallmark of general-purpose computing has been the capability to run almost any, large, functionally diverse computational task on a single hardware system. General-purpose computing platforms, to date, have largely been been built around one or more moderately coarse-grained, fixed processors. As available silicon density increases, it is worthwhile to consider other computing structures for providing flexible computation. In this paper, we look specifically at both conventional processors and reconfigurable logic to understand their relative merits in general-purpose computing scenarios. A simple analysis of delivered functional capacity suggests that conventional processors are best suited for tasks which require a diverse set of operations which are well matched to the...

110736. Explicit Provability And Constructive Semantics - Sergei N. Artemov
We find a complete axiomatization of the logic LP of propositions and proofs anticipated by Kolmogorov and Gödel. We apply LP to solve two closely related problems. In 1933 Gödel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. We give a solution to this problem by showing that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which resisted formalization since the...

110737. Default Rules: An Extension of Constructive Negation for Narrowing-based Languages
In this paper an extension of narrowing-based functional logic languages is proposed: Every partial definition of a function can be completed with a default rule. In a concrete function call, the default rule is applicable when the normal ones determine that they cannot compute the value of the call. The use of the default rule, in the presence of a goal with variables, is constructive. The operational semantics provides constraints to the variables to make the default rule applicable. Narrowing semantics are modified extending the technique of constructive negation [3, 4, 17]. 1 Introduction Narrowing is a unification based parameter passing mechanism which subsumes rewriting and SLD resolution. Different versions...

110738. Proving Termination of GHC Programs - M. R. K. Krishna Rao,D. Kapur,R. K. Shyamasundar
A transformational approach for proving termination of parallel logic programs such as GHC programs is proposed. A transformation from GHC programs to term rewriting systems is developed; it exploits the fact that unications in GHC-resolution correspond to matchings. The termination of a GHC program for a class of queries is implied by the termination of the resulting rewrite system. This approach facilitates the applicability of a wide range of termination techniques developed for rewrite systems in proving termination of GHC programs. The method consists of three steps: (a) deriving moding information from a given GHC program, (b) transforming the GHC program into a term rewriting system using...

110739. Modal Logics and Topological Semantics for Hybrid Systems - S. N. Artemov,J. M. Davoren
In this paper, we introduce the logic of a control action S4F and the logic of a continuous control action S4C on the state space of a dynamical system. The state space here is represented by a topological space (X; T ) and the control action by a function f from X to X. We present an intended topological semantics and a Kripke semantics, give both a Hilbert-style and Gentzen-style axiomatization for S4F and S4C, prove completeness with respect to both semantics as well as a cut-elimination for the corresponding sequent calculi and show the logics to be decidable. 1 Introduction Let L2 be the propositional modal language...

110740. HOHFELD in CYBERSPACE - and other applications of normative reasoning in agent technology - Christen Krogh,Henning Herrestad
Two areas of importance for agents and multiagent systems are investigated: design of agent programming languages, and design of agent communication languages. The paper contributes in the above mentioned areas by demonstrating improved or novel applications for deontic logic and normative reasoning. Examples are taken from computer-supported cooperative work, and electronic commerce. Keywords: Agents. User interface metaphors. Agent programming languages. Agent communication languages. Agent protocols. Hohfeld. Formal theories of rights. Normative structures. Deontic logic. Groupware. CSCW. Electronic Commerce. 1 Preamble The [agent] metaphor has become so pervasive that we're waiting for some enterprising company to advertise its computer switches as...

 

Busque un recurso