Thursday, April 24, 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 128,052

110721. An Exact Constraint Logic Programming Algorithm for the Traveling Salesman Problem with Time Windows - Gilles Pesant,Michel Gendreau,Jean-yves Potvin,Jean-marc Rousseau
This paper presents a constraint logic programming model for the traveling salesman problem with time windows which yields an exact branchand -bound optimization algorithm without any restrictive assumption on the time windows. Unlike dynamic programming approaches whose performance relies heavily on the degree of discretization applied to the data, our algorithm does not suffer from such space-complexity issues. The data-driven mechanism at its core more fully exploits pruning rules developed in operations research by using them not only a priori but also dynamically during the search. Computational results are reported and comparisons are made with both exact and heuristic algorithms. On Solomon's well-known test bed, our algorithm is instrumental in...

110722. Adaptive Extensions to a Multi-Branch Run-to-Run Controller for Plasma Etching - James R. Moyne,Nauman Chaudhry
Fuzzy logic and database learning mechanisms have been incorporated into a generic plasma etching run-to-run controller, resulting in a very dynamic, adaptable and robust system. The system features an Applied 8300 RIE controlled by a Techware II equipment controller. A TCP/IP connection links this equipment controller to the run-to-run controller residing on a SUN. The run-to-run control environment is generic in that the basic control framework and controller development results are applicable to VLSI manufacturing in general. The controller is multi-branch as it utilizes multiple algorithms in complementary fashion to achieve process optimization and control. The current implementation utilizes three branches: (1) a linear approximation control algorithm, (2) an...

110723. A Logic for Concurrent Events and Action Failure - David Morley,Liz Sonenberg
When reasoning about agents interacting in a dynamic world, two problems present themselves: other events and actions may occur while an agent is acting; and an agent's actions may fail. We present a more expressive formalism for representing the different ways that events can occur together and extend a recently introduced logic of events to handle concurrent events. We apply the approach of Traverso and Spalazzi to handle actions and failure to obtain a logic that allows for concurrent events and admits reasoning with failure. 1 Introduction Reasoning about the actions of autonomous agents has been a problem of continuing interest to researchers in AI. When agents are...

110724. Deriving Partial Correctness Logics From Evolving Algebras - Arnd Poetzsch--heffter
Introduction This extended abstract gives an introduction into the development of partial correctness logics for programming languages specified by evolving algebras. A partial correctness logic is a programming logic that allows to prove program properties of the form: "whenever program point P is reached during execution, assertion A is true". We derive a basic axiom (schema) from an evolving algebra and use this axiom to prove more convenient logics correct. This work aims to develop the foundations for programming environments that support formal reasoning about programs. One of the major problems with this challenge is the systematic design of programming logics for realistic programming languages. Experiences e.g. with Hoare logic...

110725. Towards Integrating Partial Evaluation in a Specialization Framework based on Generic Abstract Interpretation (Extended Abstract)
Interpretation Germ'an Puebla John Gallagher y Manuel Hermenegildo (Extended Abstract) 1 Introduction Partial evaluation [JGS93, DGT96] specializes programs for known values of the input. Partial evaluation of logic programs has received considerable attention [Neu90, LS91, Sah93, Gal93, Leu97] and several algorithms parameterized by different control strategies have been proposed which produce useful partial evaluations of programs. Regarding the correctness of such transformations, two conditions, defined on the set of atoms to be partially evaluated, have been identified which which ensure correctness of the transformation: "closedness" and "independence" [LS91]. From a practical point of view, effectiveness, that is, finding suitable control strategies which provide an appropriate level of specialization while ensuring termination, is a crucial...

110726. A Quadratic Optimiser in a Constraint Logic Programming Paradigm
This paper presents a quadratic optimiser for solving quadratic programming optimisation problem in constraint logic programming paradigm. Quadratic programming optimisation problems are a subclass of the general nonlinear programming optimisation problems in operational research. The optimiser showed fast convergence over the tested problems. It enriched the CLP(R) in Sicstus Prolog with the capability of quadratic programming optimisation in addition to the existing capability of linear programming optimisation which opens further domain of applications to CLP. Moreover, it could be extended to be used by successive quadratic programming method to solve a large class of nonlinear optimisation problems. Introduction Logic programming (LP) languages are a form of declarative languages based on...

110727. Interpolation, Preservation, and Pebble Games - Jon Barwise,Johan Van Benthem
Preservation and interpolation results are obtained for L1! and sublogics L ` L1! such that equivalence in L can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms. 1 Introduction In the heyday of infinitary logic in the 1960's and 70's, most attention was focused on L!1! and its fragments (see e.g. Keisler [19]), since countable formulas seemed best behaved. The past decade has seen a renewed interest in L1! and its finite variable fragments L (k) 1! (for 2 k ! !) and the modal fragment L Pi 1! (see e.g. Ebbinghaus and Flum [17] on the former and Barwise and Moss [9] on the latter), due to various connections...

110728. Simulation and Analysis of Business Processes Using GOLOG - Dimitris Plexousakis
This paper describes a novel approach to simulating and analyzing business processes using GOLOG, a high-level logic programming language suitable for defining complex behaviors and capable of simulating action execution. The language is based on an extended version of the situation calculus and incorporates a formal theory of action. Business processes can be viewed as actions (physical or perceptual) that affect the state of affairs or an agent's knowledge of this state. Using GOLOG, business processes can be specified, synthesized and tested for feasibility and consistency. The theoretical framework behind GOLOG includes a solution to the frame problem for perceptual and complex actions, as well as, a formal method for process analysis. The...

110729. Some Monoidal Closed Categories of Stable Domains and Event Structures - Guo-qiang Zhang
This paper introduces the following new constructions on stable domains and event structures: the tensor product, the linear function space, and the exponential. It gives rise to a monoidal closed category of dI-domains as well as one of stable event structures which can be used to interpret intuitionistic linear logic. Finally, the usefulness of the category of stable event structures for modeling concurrency and its relation to other models are discussed. CONTENTS

110730. An Agent Architecture That Combines Backward and Forward Reasoning - R. A. Kowalski,F. Sadri,F. Toni
. We present a proof procedure that combines backward reasoning with logic programs and forward reasoning with integrity constraints. We illustrate the use of the proof procedure as the inference engine underlying agents. Roughly speaking, the backward reasoning component of the proof procedure is responsible for the deliberative behaviour of agents, whereas the forward reasoning component is responsible for their reactive behaviour. 1 Introduction Recent years have seen a shift in the treatment of agents in artificial intelligence. In conventional approaches, intelligent agents reason and plan within a closed environment, producing a complete plan before they start executing it. In more recent, and arguably more realistic approaches, intelligent agents reason and plan...

110731. Programming Languages for Distributed Applications - Seif Haridi,Peter Van Roy,Christian Schulte
Much progress has been made in distributed computing in the areas of distribution structure, open computing, fault tolerance, and security. Yet, writing distributed applications remains difficult because the programmer has to manage models of these areas explicitly. A major challenge is to integrate the four models into a coherent development platform. Such a platform should make it possible to cleanly separate an application's functionality from the other four concerns. Concurrent constraint programming, an evolution of concurrent logic programming, has both the expressiveness and the formal foundation needed to attempt this integration. As a first step, we have designed and built a platform that separates an application's functionality...

110732. The Logic of Propagation in The Inscape Environment - Dewayne E. Perry
The Inscape Environment research project addresses issues in supporting the development of large systems by large numbers of programmers. One aspect of this research is the "constructive use" of formal module interface specifications - that is, given that you have formal specifications, what can you do with them. In Inscape, the specifications form the basis for providing an environment that is knowledgeable about the process of developing and evolving software systems, an environment that works in symbiosis with the programmer to develop and evolve a software system. In this discussion, I present how Inscape uses operation specifications (based on Hoare's input/output predicate approach) as the basis for synthesizing the interfaces for such...

110733. Dyana --- The Pilot Project For Investigation Of Distributed Programs And Computer Systems - A. G. Bakhmurov,R. L. Smeliansky
The tool of distributed computer environment simulation and analysis is described. The key features of this tool are: the possibility of both quantitative and algorithmic analysis of system to be modeled; the time complexity estimation subsystem which helps to avoid the instruction-level simulation of target computer system. A model development language overview is presented. Certain attention is paid to the algorithmic analysys and specification features along with the technology of model development. Keywords: Simulation, performance analysis, distributed computer systems, temporal logic 1. Introduction The DYANA system (DYnamic ANAlyzer) is the software system which is proposed to help analyze distributed computer environment operation. The design and development of the system were aimed at...

110734. Strictness Analysis in Logical Form - Thomas P. Jensen
This paper presents a framework for comparing two strictness analysis techniques: Abstract interpretation and non--standard type inference. The comparison is based on the representation of a lattice by its ideals. A formal system for deducing inclusions between ideals of a lattice is presented and proved sound and complete. Viewing the ideals as strictness properties we use the formal system to define a program logic for deducing strictness properties of expressions in a typed lambda calculus. This strictness logic is shown to be sound and complete with respect to the abstract interpretation, which establishes the main result that strictness analysis by type--inference and by abstract interpretation are equally powerful...

110735. Confinement Properties for Programming Languages - Dennis Volpano,Geoffrey Smith
ation is to use digital signatures. Here you would verify a digital signature that is computed over the program using TrustMe's private key. But this is not much help in the scenario above. It merely provides you with confirmation that the program came from TrustMe so that they can be held accountable if some day you discover that the program did misbehave. By that time there is no telling how many "data warehouses" [13] already store the information. To appear in SIGACT News, 1998 But suppose we have a formal system, or logic, in which to reason about a program's ability to preserve privacy. Then our trust in...

110736. Techniques for Preventing Recomputation in Logic Programs - Paulo Jorge,Sousa Azevedo
In this thesis we investigate techniques for preventing recomputation in the execution of logic programs. One can reduce recomputation by eliminating subquery redundancy. This can be achieved by storing intermediate results, which are shared between identical subqueries. This is known as the tabulation technique. We consider top-down evaluation procedures incorporating a tabulation or `lemmatization' mechanism and also bottom-up evaluation with goal orientation, as exemplified by the `magic sets' transformation. By assessing these two forms of evaluation and by pointing out some relationships between them we proceed towards a recomputation-free evaluation. Several top-down evaluation strategies that use tabulation have been proposed in the literature. However, all of these mechanisms...

110737. Higher-Order Logic Programming as Constraint Logic Programming - Spiro Michaylov,Frank Pfenning
Higher-order logic programming (HOLP) languages are particularly useful for various kinds of metaprogramming and theorem proving tasks because of the logical support for variable binding via - abstraction. They have been used for a wide range of applications including theorem proving, programming language interpretation, type inference, compilation, and natural language parsing. Despite their utility, current language implementations have acquired a well-deserved reputation for being inefficient. In this paper we argue that HOLP languages can reasonably be viewed as Constraint Logic Programming (CLP) languages, and show how this can be expected to lead to more practical implementations by applying the known principles for the design and implementation of...

110738. Constructive Natural Deduction And Its "omega-Set" Interpretation - Eugenio Moggi
. Various Theories of Types are introduced, by stressing the analogy "propositionsas -types" : from propositional to higher order types (and Logic). In accordance with this, proofs are described as terms of various calculi, in particular of polymorphic (second order) l- calculus. A semantic explanation is then given by interpreting individual types and the collection of all types in two simple categories built out of the natural numbers (the modest sets and the universe of w-sets). The first part of this paper (syntax) may be viewed as a short tutorial with a constructive understanding of the deduction theorem and some work on the expressive power of first...

110739. Introducing Some Classical Elements of Modal Logic to the Propositional Logics of Qualitative Probabilities - Dimitar P. Gelev
This paper presents the construction of canonical models for a number of logics of qualitative probabilities by introducing a conservative infinitary rule into their axiomatizations. These logics include the minimal logic of qualitative probabilities [Seg71, Gar75] and a new multioperator propositional logic, that contains qualitative probabilistic analogons of operations essential to propositional dynamic logic. These operations capture some basic laws for stochastic processes into this new logic's semantics and are given a complete axiomatization. The paper also presents qualitative probabilistic versions of the modal logic techniques of unravelling and filtration. All the constructs and arguments in this paper are suitable to be combined with their counterparts for other propositional, e.g....

110740. Local Specification of Distributed Families of Sequential Objects - Hans-dieter Ehrich
. Fully concurrent models of distributed object systems are specified using linear temporal logic that does not per se cope with concurrency. This is achieved by employing the principle of local sequentiality: we specify from local viewpoints assuming that there is no intraobject concurrency but full inter-object concurrency. Local formulae are labelled by identity terms. For interaction, objects may refer to actions of other objects, e.g., calling them to happen synchronously. A locality predicate allows for making local statements about other objects. The interpretation structures are global webs of local life cycles, glued together at shared communication events. These interpretation structures are embedded in an interpretation frame that is a...

 

Busque un recurso