Wednesday, September 3, 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 130,671

110721. Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System. - Alessandro Cimatti,Fausto Giunchiglia,Giorgio Mongardi,Dario Romano,Fernando Torielli,Paolo Traverso,Ansaldo Segnalamento Ferroviario (asf,Ansaldo Trasporti (atr
This paper reports on an experience in formal verification using spin. The analyzed system is the Safety Logic of an interlocking system for the control of railway stations developed by Ansaldo. The Safety Logic is a process-based software architecture, which can be configured to implement different functions and control stations of different topology. In this paper we describe how a promela model has been devised, which retains the configurability features of this architecture. Furthermore, we discuss the verification with spin of significant process configurations. 1 Introduction This paper describes a joint project between Ansaldo and IRST. The goal of the project was the evaluation of the possibility to integrate formal...

110722. The Practice of Logical Frameworks - Frank Pfenning
Introduction Deductive systems, given via axioms and rules of inference, are a common conceptual tool in mathematical logic and computer science. They are used to specify many varieties of logics and logical theories as well as aspects of programming languages such as type systems or operational semantics. A logical framework is a meta-language for the specification of deductive systems. Research on logical frameworks is still in its infancy. Nonetheless, different frameworks have been proposed, implemented, and applied to a variety of problems. In addition, some general reasoning systems have been used to study deductions as mathematical objects, without specific support for the domain of deductive systems. This short survey cannot...

110723. A Logical View Of Concurrent Constraint Programming - Nax P. Mendler,Prakash Panangaden,P. J. Scott,R. A. G. Seely
. Concurrent Constraint Programming (CCP) has been the subject of growing interest as the focus of a new paradigm for concurrent computation. Like logic programming it claims close relations to logic. In fact CCP languages are logics in a certain sense that we make precise in this paper. In recent work it was shown that the denotational semantics of determinate concurrent constraint programming languages forms a fibred categorical structure called a hyperdoctrine, which is used as the basis of the categorical formulation of first-order logic. What this shows is that the combinators of determinate CCP can be viewed as logical connectives. In this paper we extend these ideas...

110724. Natural Deduction for Intuitionistic Non-Commutative Linear Logic - Jeff Polakow
. We present a system of natural deduction and associated term calculus for intuitionistic non-commutative linear logic (INCLL) as a conservative extension of intuitionistic linear logic. We prove subject reduction and the existence of canonical forms in the implicational fragment. We also illustrate by means of an example how the proof term calculus can be employed in the setting of logical frameworks to capture useful representation invariants. 1 Introduction Intuitionistic logic captures pure functional computation in a logical way, as can be seen from the Curry-Howard isomorphism between constructive proofs and functional programs. However, there are many structural properties of programs that are not captured within the intuitionistic framework, such as...

110725. Termination Analysis for Partial Functions - Jurgen Brauburger,Jurgen Giesl
. This paper deals with automated termination analysis for partial functional programs, i.e. for functional programs which do not terminate for each input. We present a method to determine their domains (resp. non-trivial subsets of their domains) automatically. More precisely, for each functional program a termination predicate algorithm is synthesized, which only returns true for inputs where the program is terminating. To ease subsequent reasoning about the generated termination predicates we also present a procedure for their simplification. 1 Introduction Termination of algorithms is a central problem in software development and formal methods for termination analysis are essential for program verification. While most work on the automation of termination proofs has...

110726. Disjunctive Chronolog - Disjunctive Chronolog Gergatsoulis,T. Panayiotopoulos
A disjunctive temporal logic programming language, called Disjunctive Chronolog is presented in this paper. Disjunctive Chronolog combines the ideas of both temporal logic programming and disjunctive logic programming. The new language is capable of expressing dynamic behaviour as well as uncertainty, two notions that are very common in a variety of real systems. Minimal model semantics, model state semantics and øxpoint semantics are developed for the proposed language and their equivalence is shown. Keywords: Temporal logic programming, disjunctive logic programming. 1 Introduction Temporal logic programming[OM94, Org91] has been widely used as a means for describing systems that are inherently dynamic. For example, consider the following Chronolog[Wad88] program simulating the operation...

110727. Towards an infinitary logic of domains: Abramsky logic for transition systems - Marcello M. Bonsangue,Joost N. Kok
We give a new characterization of sober spaces in terms of their completely distributive lattice of saturated sets. This characterization is used to extend Abramsky's results about a domain logic for transition systems. The Lindenbaum algebra generated by the Abramsky finitary logic is a distributive lattice dual to an SFP-domain obtained as a solution of a recursive domain equation. We prove that the Lindenbaum algebra generated by the infinitary logic is a completely distributive lattice dual to the same SFP-domain. As a consequence soundness and completeness of the infinitary logic is obtained for a class of transition systems that is computational interesting. 1 Introduction Complete partial orders were originally...

110728. Formal Methods and the Certification of Critical Systems - John Rushby
This report was prepared to supplement a forthcoming chapter on formal methods in the FAA Digital Systems Validation Handbook 1 . Its purpose is to outline the technical basis for formal methods in computer science, to explain the use of formal methods in the specification and verification of software and hardware requirements, designs, and implementations, to identify the benefits, weaknesses, and difficulties in applying these methods to digital systems used in critical applications, and to suggest factors for consideration when formal methods are offered in support of certification. The report assumes a serious interest in the engineering of critical systems, and a willingness to read occasional mathematical formulas and specialized terminology, but...

110729. Performance Prediction for the HTMT: A Programming Example - Jose Nelson Amaral,Guang R. Gao,Phillip Merkey,Thomas Sterling,Zachary Ruiz,Sean Ryan
This paper presents an analytical performance prediction for the implementation of Cannon's matrix multiply algorithm in the Hybrid Technology Multi-Threading (HTMT) architecture [8]. The HTMT subsystems are built from new technologies: super-conducting processor elements (called SPELLs [5]), a network based on RSFQ (Rapid Single Flux Quantum) logic devices (called

110730. Dependence Speculative Multithreaded Architecture - Pedro Marcuello
Boosting instruction level parallelism in dynamically scheduled processors requires a large instruction window. The approach taken by current superscalar processors to build the instruction window is known to have important limitations, such as the requirement of more powerful instruction fetch mechanisms and the increasing complexity and delay of the issue logic. In this paper we present a novel processor architectures (which is called DeSM) that takes a completely different approach to build a large instruction window. The idea is to identify at run-time sections of code that correspond to loops and execute concurrently several iterations even if they are dependent. Unlike superscalar processors, instructions are not...

110731. Learning the - William W. Cohen,Haym Hirsh
We present a series of theoretical and experimental results on the learnability of description logics. We first extend previous formal learnability results on simple description logics to C-Classic, a description logic expressive enough to be practically useful. We then experimentally evaluate two extensions of a learning algorithm suggested by the formal analysis. The first extension learns C-Classic descriptions from individuals. (The formal results assume that examples are themselves descriptions.) The second extension learns disjunctions of C-Classic descriptions from individuals. The experiments, which were conducted using several hundred target concepts from a number of domains, indicate that both extensions reliably learn complex natural concepts. 1 INTRODUCTION One well-known family of formalisms for representing knowledge are description logics, sometimes also called terminological logics...

110732. First Order Linear Logic Without Modalities is NEXPTIME-Hard - Patrick Lincoln,Andre Scedrov
The decision problem is studied for the nonmodal or multiplicative-additive fragment of first order linear logic. This fragment is shown to be nexptime- hard. The hardness proof combines Shapiro's logic programming simulation of nondeterministic Turing machines with the standard proof of the pspace- hardness of quantified boolean formula validity, utilizing some of the surprisingly powerful and expressive machinery of linear logic. 1 Introduction Linear logic, introduced by Girard, is a resource-sensitive refinement of classical logic [10, 29]. Linear logic gains its expressive power by restricting the "structural" proof rules of contraction (copying) and weakening (erasing). The contraction rule makes it possible to reuse any stated assumption as often as desired. The...

110733. The Hyperfinite Signal: Application To The Modelling Of Discrete Events Systems Behaviour - Jean-paul Frachet,Rine Lamperiere,Jean-marc Faure
The notion of hyperfinite signal enables to describe the temporal evolution of a discrete value in a formalism similar to the one of continuous values evolving in a continuous time. It relies on an original model of time and discrete values. A subtype allows the modelling of discrete events systems. Keywords Grafcet, behaviour, temporal logic, non standard analysis, finite-dimensional fields 1. OBSERVATION OF THE TEMPORAL EVOLUTION OF A PHENOMENON The time evolution of physical values can be described, formally or informally, by a function x = f(t) where x is the modelling of a value and t is the modelling of the time. In the natural sciences such as physics or mechanics, a phenomenon...

110734. Equational Inference, Canonical Proofs, And Proof Orderings - Leo Bachmair,Nachum Dershowitz
We describe the application of proof orderings---a technique for reasoning about inference systems---to various rewrite-based theorem-proving methods, including refinements of the standard Knuth-Bendix completion procedure based on critical pair criteria; Huet's procedure for rewriting modulo a congruence; ordered completion (a refutationally complete extension of standard completion); and a proof by consistency procedure for proving inductive theorems. This is a substantially revised version of the paper, "Orderings for equational proofs," co-authored with J. Hsiang and presented at the Symp. on Logic in Computer Science (Boston, Massachusetts, June 1986). It includes material from the paper "Proof by consistency in equational theories," by the first author, presented at the Third...

110735. Specifications with Observable Formulae and Observational Satisfaction Relation - Teodor Knapik
We consider algebraic specifications with observational features. Axioms as well as observations are formulae of full (ManySorted) First Order Logic with Equality. The associated semantics is based on a non standard interpretation of equality called observational equality. We study the adequacy of this semantics for software specification and the relationship with behavioural equivalence of algebras. We show that this framework defines an institution. Keywords: algebraic specification, observability, semantics. 1 Introduction Within an observational approach the loose semantics of a specification may either be defined as a class of algebras observationally equivalent to models satisfying the specification in the usual sense or as a class of algebras observationally satisfying the specification. The former...

110736. A Proof Theoretic View of Constraint Programming - Krzysztof R. Apt
. We provide here a proof theoretic account of constraint programming that attempts to capture the essential ingredients of this programming style. We exemplify it by presenting proof rules for linear constraints over interval domains, and illustrate their use by analyzing the constraint propagation process for the SEND + MORE = MONEY puzzle. We also show how this approach allows one to build new constraint solvers. Keywords: constraints, constraint propagation, proof rules, linear constraints. 1. Introduction 1.1. Motivation One of the most interesting recent developments in the area of programming has been constraint programming. A prominent instance of it is constraint logic programming exemplified by such programming languages as CLP(R),...

110737. Constraint Oriented Specification for Timed CSP - Jeremy Bryans
A popular specification style, particularly for the initial specification of a system, is the constraint-oriented style; for example specifying temporal and behavioural aspects separately. While this style is appealing, it can be hard to apply in practice, because languages which are designed to describe easily one type of constraint are not always able to easily capture another type. In this paper, we develop a framework in which a specification is a pair (P ; OE), where P is a CSP process and OE is a formula of Propositional Temporal Logic (PTL). CSP (Communicating Sequential Processes) is a process-algebraic language designed for the specification and analysis of parallel...

110738. Well-Founded Semantics for Extended Logic Programs with Dynamic Preferences - Gerhard Brewka,Tu Wien,Abteilung Fur Wissensbasierte Systeme
The paper describes an extension of well-founded semantics for logic programs with two types of negation. In this extension information about preferences between rules can be expressed in the logical language and derived dynamically. This is achieved by using a reserved predicate symbol and a naming technique. Conflicts among rules are resolved whenever possible on the basis of derived preference information. The well-founded conclusions of prioritized logic programs can be computed in polynomial time. A legal reasoning example illustrates the usefulness of the approach. 1. Introduction: Why Dynamic Preferences are Needed Preferences among defaults play a crucial role in nonmonotonic reasoning. One source of preferences that has been studied...

110739. Simulation, Theory, and Cut Elimination - Dr. G. White
This paper is concerned with the contrast between simulation- and deduction-based approaches to reasoning about physical objects. We show that linear logic can give a unified account of both simulation and deduction concerning physical objects; it also allows us to draw a principled distinction between simulation and deduction, since simulations correspond to cut-free proofs, whereas deductions correspond to proofs in general. During the preparation of this work, the author was paid by Project Dynamo, supported by the United Kingdom Engineering and Physical Sciences Research Council under grant number GR/K 19266. The views expressed in this paper are the author's own, and the principal investigators of the project -- John Bell...

110740. Autonomous Navigation using an Adaptive Hierarchy of Multiple Fuzzy-Behaviors - Edward Tunstel,H. Danny,M. Jamshidi
Adaptive behavioral capabilities are necessary for robust mobile robot navigation in non-engineered environments. Robust behavior requires that uncertainty be accommodated in the robot control system, especially when autonomy is desired. Fuzzy logic control technology enables development of controllers which can provide the necessary computational intelligence in real-time. This paper presents the incorporation of fuzzy logic, into the framework of behavior-based control. An architecture for hierarchical behavior control is presented in which control decisions result from a consensus of behavioral recommendations. Multiple fuzzy-behavior coordination is discussed and applied to autonomous navigation without explicit maps. Performance and robustness is demonstrated by implementation on a mobile robot with significant mechanical imperfections. 1 Introduction Motion control solutions for mobile robotics are being sought...

 

Busque un recurso