Friday, March 6, 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 140,063

110721. A New Approach for Specification and Verification of Distributed Agents - Andrew M. Mironov,Virendra C. Bhavsar
We propose a language for formal description of distributed agents and introduce a new approach to their specification. The specification language uses the concept of a fixpoint construction, which is a generalization of temporal operators in temporal logic. With the proposed formalism we are also able to construct correctness proofs for distributed agents. The verification technique is a generalization of the Floyd's inductive assertion method. Keywords: distributed agents, specification, verification, assertions, fixpoint construction. 1 Introduction The problem of specification and formal verification of distributed communicating systems (DCS) is one of most important problems in theoretical computer science. DCSs arise in a wide range of applications, for example in distributed information processing, telecommunications, control of complex systems...

110722. A Calculus for Interrogatives Based on Their Algebraic Semantics - Rani Nelken,Nissim Francez
We present a novel calculus for reasoning with both indicative and interrogative sentences, simultaneously modeling entailment between indicative sentences, entailment between interrogative sentences and answerhood relations. The logic is based on an interpretation of questions as entities of type t, the type of propositions. This is achieved by an algebraic reinterpretation of the domain of type t as a bilattice, rather than the standard boolean interpretation. We provide a Gentzen style axiomatization of the logic and prove its soundness and completeness with respect to the bilattice semantics. We also consider an alternative formulation using multi-valued free variable first-order tableaux, allowing for e#cient algorithmic proof-search. We have implemented the...

110723. Sequents, Frames, and Completeness - Thierry Coquand
. Entailment relations, originated from Scott, have been used for describing mathematical concepts constructively and for representing categories of domains. This paper gives an analysis of the freely generated frames from entailment relations. This way, we obtain completeness results under the unifying principle of the spatiality of coherence logic. In particular, the domain of disjunctive states, derived from the hyperresolution rule as used in disjunctive logic programs, can be seen as the frame freely generated from the opposite of a sequent structure. At the categorical level, we present equivalences among the categories of sequent structures, distributive lattices, and spectral locales using appropriate morphisms. Introduction Entailment relations were introduced by Scott as an...

110724. Declarative Specification of Z39.50 Wrappers using Description Logics - Yannis Velegrakis,Vassilis Christophides,Panos Constantopoulos
. Z39.50 is a client#server protocol widely used in digital libraries and museums for searching and retrieving information spread over anumber of heterogeneous sources. Toovercome semantic and schematic discrepancies among the various data sources the protocol relies on a world view of information as a #at list of #elds, called Access Points #AP#. One of the major issues for building Z39.50 wrappers is to map this unstructured list of APs to the underlying source data. Unfortunately, existing Z39.50 wrappers have been developed from scratch and they do not provide high-level mapping languages with veri#able properties. In this paper, we propose a Description Logic based toolkit for the declarative speci#cation of...

110725. Possibly Infinite Sequences in Theorem Provers: A Comparative Study - Marco Devillers,David Griffioen
. We compare four different formalizations of possibly infinite sequences in theorem provers based on higher-order logic. The formalizations have been carried out in different proof tools, namely in Gordon's HOL, in Isabelle and in PVS. The comparison considers different logics and proof infrastructures, but emphasizes on the proof principles that are available for each approach. The different formalizations discussed have been used not only to mechanize proofs of different properties of possibly infinite sequences, but also for the verification of some non-trivial theorems of concurrency theory. 1 Introduction Sequences occur frequently in all areas of computer science and mathematics. In particular, formal models of distributed systems often employ (possibly infinite) sequences...

110726. Binding-Time Analysis for Mercury - Wim Vanhoof,Maurice Bruynooghe
In this paper, we describe a binding-time analysis (BTA) for a statically typed and strongly moded pure logic programming language, in casu Mercury. Binding-time analysis is the key concept in achieving o-line program specialisation: the analysis starts from a description of the program's input available for specialisation, and propagates this information throughout the program, deriving directives for when and how to perform specialisation. Exploiting the possibilities oered by Mercury's strong type and mode system, we present a completely automatic BTA dealing with partially static binding-times. 1 Introduction Program specialisation is a well-studied source-to-source transformation, capable of optimising a program P with respect to a known part s of its input (s;...

110727. Formalising UML Use Cases in the Refinement Calculus - Ralph-johan Back,Luigia Petre,Porres Paltor,Turku Centre,Computer Science
The Unified Modeling Language (UML) consists of a set of diagrams that describe a system under development. A use case diagram specifies the required functionality of the system, showing the collaboration among a set of actors that are to perform certain tasks. We enhance use case diagrams by providing formal documents (like specifications or programs), called contracts that regulate the behaviour of the agents involved. These agents could be programs, modules, systems, users. The contract is written in a language with a precise semantics and logic for reasoning, the refinement calculus. Hence, it can be analysed for the preconditions required in order to achieve certain goals. In order to...

110728. A WAM-based implementation for Composition of Logic Programs - A. Chiarelli,V. Mazzotta,C. Renso
The main aim of this paper is to show an abstract machine for compiling logic programs composed by means of meta-operators; in particular, we deal with union, intersection and closure, which are directly supported by the most common abstract machine for logic programming: the Warren Abstract Machine. The proposed solution is a mix of the interpretation-oriented and the compilation-oriented approach such that it is possible to exploit the benefits and to reduce, as possible, the drawbacks. 1 Introduction Many extensions of logic programming have been proposed to increase its expressive power and to widen application area. Such extensions provide tools to deal with typical problems of Artificial Intelligence (hypothetical reasoning, knowledge assimilation)...

110729. Linear Logical Characterization of Polyspace Functions (Extended Abstract)
) Kazushige Terui 3 Abstract Light Linear Logic (LLL) of [Gir95] characterizes the polytime functions through a careful handling of structural inference rules of logic. Based on this purely logical approach, we give a characterization of the polyspace functions. Our logical system is an extension of Intuitionistic Light Affine Logic (ILAL) of [Asp98], a variant of LLL with full (unrestricted) weakening. We introduce the notion of split terms and enrich ILAL by allowing a !- box to be formed from a split term. The resulting system, called Intuitionistic Polyspace Affine Logic, precisely characterizes the polyspace functions. 1 Introduction Linear Logical Approach to Computational Complexity. Over the past few decades, a considerable number of studies have been made on logical characterizations of...

110730. Term-Rewriting Implementation of Equational Logic Programming - Michael J. O'donnell
In 1975 I started a small project to explore the consequences of implementing equational programs with no semantic compromises. Latest results include a compiler that executes exactly the logical consequences of an equational program, with run-time speed comparable to compiled Franz LISP. This paper describes the accomplishments of the project very briefly, concentrating on shortcomings and directions for future work. 1 Introduction The most common approach to providing semantics for programming languages is to regard a program as the definition of a collection of functions. In some cases great ingenuity is required to construct the unique function associated with each symbol in a program. Inputs and outputs are regarded as values...

110731. Residuation and Guarded Rules for Constraint Logic Programming - Gert Smolka
A major difficulty with logic programming is combinatorial explosion: since goals are solved with possibly indeterminate (i.e., branching) reductions, the resulting search trees may grow wildly. Constraint logic programming systems try to avoid combinatorial explosion by building in strong determinate (i.e., non-branching) reduction in the form of constraint simplification. In this paper, we present two concepts, residuation and guarded rules, for further strengthening determinate reduction. Both concepts apply to constraint logic programming in general and yield an operational semantics that coincides with the declarative semantics. Residuation is a control strategy giving priority to determinate reductions. Guarded rules are logical consequences of programs adding otherwise unavailable determinate reductions. R esum...

110732. First Order Linear Temporal Logic over Finite Time Structures - Serenella Cerrito,Marta Cialdea Mayer
In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTL fin , is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTL fin is not recursively axiomatizable. This negative result however does not hold in the case of bounded validity, that is truth in all temporal models where the object domain is possibly infinite, but the underlying sequence of time points does not exceed a given size. A formula is de ned to be k-valid if it is true in all temporal models whose...

110733. HyTech: A Model Checker for Hybrid Systems - Thomas A. Henzinger,Pei-hsin Ho,Howard Wong-toi
A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. HyTech is a symbolic model checker for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically by computing with polyhedral state sets. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal-logic requirement. 1 Introduction A hybrid system typically consists of a...

110734. Decision Procedure for - Fausto Giunchiglia,Roberto Sebastiani
The goal of this paper is to describe and thoroughly test a decision procedure, called Ksat, checking satisfiability in the terminological logic ALC. Ksat is said to be SATbased as it is defined in terms of a decision procedure for propositional satisfiability (SAT). The tests are performed comparing Ksat with, among other procedures, Kris, a state-of-the-art tableau-based implementation of a decision procedure for ALC. Ksat outperforms Kris of orders of magnitude. Furthermore, the empirical results highlight an intrinsic weakeness that tableau-based decision procedures have with respect to SATbased decision procedures. 1 INTRODUCTION The goal of this paper is to describe and thoroughly test a new decision procedure, called Ksat, checking satisfiability in the terminological logic ALC, as defined in...

110735. Verification of Logic Programs and Imperative Programs - Lee Naish
This paper explores the relationship between verification of logic programs and imperative programs with the aim of uncovering the kinds of reasoning used to construct logic programs. We discuss forward reasoning, such as that used for verifying imperative programs using the inductive assertion method, and backward reasoning, such as that used for verifying imperative programs using subgoal induction and logic programs using consequence verification. We argue that consequence verification is often inadequate for Prolog programs because programmers make implicit assumptions about how procedures are called. These assumptions can be made explicit using general type declarations. Verification of logic programs with type declarations can be done in two steps. We show...

110736. A Constructive Game Semantics for the Language of Linear Logic - Giorgi Japaridze
I present a semantics for the language of first order additive-multiplicative linear logic, i.e. the language of classical first order logic with two sorts of disjunction and conjunction. The semantics allows us to capture intuitions often associated with linear logic or constructivism such as sentences =games, sentences=resources or sentences=problems, where "truth" means existence of an effective winning (resource-using, problem-solving) strategy. The paper introduces a decidable first order logic ET in the above language and gives a proof of its soundness and completeness (in the full language) with respect to this semantics. Allowing noneffective strategies in the latter is shown to lead to classical logic. The semantics presented here is very similar...

110737. Preference Logics for Automated Decision Making - Vu Ha
Classical decision theory provides a normative theory for representing and reasoning with complex preferences. But straightforward application of this theory to construct automated decision making agents is difficult due to the high cost of eliciting utilities. People tend to express their preferences in qualitative terms and have troubles translating them into numeric utilities. This difficulty has recently sparked interests in studies of qualitative theories for decision making. In this paper I sample several such proposals which share the same focus on developing logic-oriented approaches to representing and reasoning with preferences.

110738. Sharing and Groundness Dependencies in Logic Programs - M. Codish,H. Sndergaard,P. J. Stuckey
We investigate Jacobs and Langen's Sharing domain for the analysis of set-sharing and show that it is isomorphic to the Pos domain, introduced by Marriott and Sndergaard for the analysis of groundness dependencies. The key idea is to view the sets of variables in a Sharing domain element as the models of a corresponding Boolean function. This leads to re-casting set-sharing analysis in terms of the property of "not being affected by the binding of a single variable." Such an "unaffectedness dependency" analysis reveals close connections with groundness dependency analysis using positive Boolean functions. The new view of set-sharing analysis improves our understanding of this type...

110739. Exploiting ILP in Page-Based Intelligent Memory - Mark Oskin,Justin Hensley,Diana Keen,Frederic T. Chong,Matthew Farrens,Aneet Chopra
This study compares the speed, area, and power of different implementations of Active Pages [OCS98], an intelligent memory system which helps bridge the growing gap between processor and memory performance by associating simple functions with each page of data. Previous investigations have shown up to 1000X speedups using a block of reconfigurable logic to implement these functions next to each subarray on a DRAM chip. In this study, we show that instruction-level parallelism, not hardware specialization, is the key to the previous success with reconfigurable logic. In order to demonstrate this fact, an Active Page implementation based upon a simplified VLIW processor was developed. Unlike conventional VLIW processors, power and area constraints lead...

110740. Pre-Layout Estimation of Individual Wire Lengths - Srinivas Bodapati,Farid N. Najm
We present a novel technique for estimating individual wire lengths in a given standardcell -based design during the technology mapping phase of logic synthesis. The proposed method is based on creating a black box model of the place and route tool as a function of a number of parameters which are all available before layout. The place and route tool is characterized, only once, by applying it to a set of typical designs in a certain technology. We also propose a net bounding box estimation technique based on the layout style and net neighborhood analysis. We show that there is inherent variability in wire lengths obtained using commercially available place and route tools...

 

Busque un recurso