Wednesday, October 7, 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 150,248

110721. Call-By-Value Games - Samson Abramsky,Guy Mccusker
A general construction of models of call-by-value from models of callby -name computation is described. The construction relies on the fact that common denotational models of programming languages are also models of linear logic. When applied to categories of games, it yields fully abstract models of the call-by-value functional language PCFv and of a language with imperative features similar to the references of Standard ML.

110722. A Genetic Programming Approach to Logic Function Synthesis by means of Multiplexers - Arturo Hern'andez Aguirre,Carlos A. Coello Coello,Bill P. Buckles
This paper presents an approach based on the use of genetic programming to synthesize logic functions. The proposed approach uses the 1-control line multiplexer as the only design unit, defining any logic function (defined by a truth table) through the replication of this single unit. Our fitness function first explores the search space trying to find a feasible design and then concentrates in the minimization of such (fully feasible) circuit. The proposed approach is illustrated using several sample Boolean functions.

110723. Multi-Modal Control of Systems with Constraints - T. John Koo,Shankar Sastry
In multi-modal control paradigm, a set of controllers of satisfactory performance have already been designed and must be used. Each controller may be designed for a di#erent set of outputs in order to meet the given performance objectives and system constraints. When such a collection of control modes is available, an important problem is to be able to accomplish a variety of high level tasks by appropriately switching between the low-level control modes. In this paper, we propose a framework for determining the sequence of control modes that will satisfy reachability tasks. Our framework exploits the structure of output tracking controllers in order to extract a finite graph where the mode switching problem...

110724. Doing Two-Level Logic Minimization - Olivier Coudert
Two-level logic minimization consists in finding a minimal cost sum-of-products, i.e, disjunctive normal form, of a given Boolean function. This paper presents a new algorithm to solve this problem, and gives experimental evidences showing that it outperforms the leading minimizers of several orders of magnitude. We suspect that it may be possible to explain this improvement in performance theoretically, and hope that our empirical results will stimulate research along these line.

110725. Analysing resource use in the A-calculus by type inference - S. A. Courtenage,C. D. Clack
If we view functions as processes, then their resources are their arguments, supplied through application, and used by the function to produce a result. In this paper, we define resource use for functions, based on the syntactic notion of needed redexes from [BKKS86]. We introduce a variant of neededhess, tail-neededness, and define packets of needed descendants of redexes in order to mea- sure the degree of neededhess. These results are generalised to produce a semantic characterisation of the resource use properties of functions, using a term-model. By means of the Curry-Howard isomorphism, we apply these ideas to proof trees of propositions in Intuitionistic Logic to demonstrate that propositions, i.e. types, can be used to express...

110726. PVS: Combining Specification, Proof Checking, - S. Owre,S. Rajan,J. M. Rushby,N. Shankar,M. Srivas
typed higher-order logic, but the type system has been augmented with subtypes and dependent types. Though typechecking is undecidable for the PVS type system, the PVS typechecker automatically checks for simple type correctness and generates proof obligations corresponding to predicate subtypes. These proof obligations can be discharged through the use of the PVS proof checker. PVS also has parametric theories so that it is possible to capture, say, the notion of sorting with respect to arbitrary sizes, types, and ordering relations. By exploiting subtyping, dependent typing, and parametric theories, researchers at NASA Langley Research Center and SRI have developed a very general bit-vector library. Paul Miner at NASA The development...

110727. Actors, Actions, and Initiative in Nor- - R. J. Wieringa,J. -j. Ch. Meyer
The logic of norms, called deontic logic, has been used to specify normative constraints for information systems. For example, one can specify in deontic logic the constraints that a book borrowed from a library should be returned within three weeks, and that if it is not returned, the library should send a reminder. Thus, the notion of obligation to perform an action arises naturally in system specification.

110728. A New Class of Decidable Hybrid Systems - Gerardo Laerriere,Sergio Yovine
One of the most important analysis problems of hybrid systems is the reachability problem. State of the art computational tools perform reachability computation for timed automata, multirate automata, and rectangular automata. In this paper, we extend the decidability frontier for classes of linear hybrid systems, which are introduced as hybrid systems with linear vector fields in each discrete location. This result is achieved by showing that any such hybrid system admits a finite bisimulation, and by providing an algorithm that computes it using decision methods from mathematical logic.

110729. A Structured Logic Programming Approach - Enrico Denti,Antonio Natali,Andrea Omicini,Francesco Zanichelli
This paper discusses an approach to robot programming based on Prolog, properly extended with control capabilities toward program structuring (contextual programming) and (pseudo)concurrence (communicating Prolog units). This Prolog-based programming system supports the definition, both static and dynamic, of extendible software components, promoting at the same time incremental design and development of software systems. Moreover, it suggests an approach to integration between object-oriented, knowledge-based and logic programming, introducing powerful concepts such as backtrackable objects and dynamic object configuration. Finally, the system, which is embedded in a simple architecture constituted by several Prolog machines sharing a data-base acting as an evolving world, provides an effective way to reduce the gap...

110730. A Mini-course on Temporal Databases - David Toman
Temporal Databases 9 Basic Building Blocks 10 The Snapshot Model 11 Snapshots: Example 12 Histories 13 The Timestamp Model 14 Timestamp Example 15 Query Languages 16 First-order Temporal Connectives 17 Examples of Temporal Connectives 18 Propositional Temporal Logic 19 First-order Temporal Logic: syntax 20 FOTL: semantics 21 Examples 22 Temporal Relational Calculus: syntax 23 Temporal RC: Semantics 24 Examples 25 Examples (cont.) 26 Expressive Power 27 Expressive Power (cont.) 28 How do we prove it? 29 Scope of Temporal Variables 30 Ehrenfeucht-Frassb Games 31 Ehrenfeucht-Frassb Games (cont.) 32 Ehrenfeucht-Frassb Games (cont.) 33 Ehrenfeucht-Frassb Games (cont.) 34 EF Games and Temporal Logic 35 Compatibility of Variables in FOTL 36 Databases not distinguishable by FOTL 37 Communication Complexity 38 Consequences for Temporal Queries 39 Temporal Relational Algebra 40 TRA: example 41 Temporal Logic TL(FO) 42 Plan 43...

110731. Using Logic for Querying XML Data - Nick Bassiliades,Ioannis Vlahavas,Dimitrios Sampson
In this chapter, we propose the use of first-order logic, in the form of deductive database rules, as a query language for XML data and we present X-DEVICE, an extension of the deductive object-oriented database system DEVICE for storing and querying XML data. XML documents are stored into the OODB by automatically mapping the DTD to an object schema. XML elements are treated either as classes or attributes based on their complexity, without loosing the relative order of elements in the original document. Furthermore, this chapter describes the extension of the system's deductive rule query language with second-order variables, general path and ordering expressions, for querying...

110732. An Algebraic Perspective of Constraint Logic Programming - Ra Di Pierro
We develop a denotational, fully abstract semantics for constraint logic programming (clp) with respect to successful and failed observables. The denotational approach turns out very useful for the definition of new operators on the language as the counterpart of some abstract operations on the denotational domain. In particular, by defining our domain as a cylindric Heyting algebra, we can exploit, to this aim, operations of both cylindric algebras (such as cylindrification), and Heyting algebras (such as implication and negation). The former allows us to generalize the clp language by introducing an explicit hiding operator; the latter allows us to define a notion of negation which extends the classical...

110733. Multiple Model Adaptive Control, Part 2: Switching - Jogo Hespanha,Daniel Liberzonll,A. Stephen Morse,Brian D. O. Anderson,Thomas S. Brinsmead,Franky De Bruyne
This paper addresses the problem of controlling a continuous-time linear system with large modeling errors. We employ an adaptive control algorithm consisting of a family of linear candidate controllers supervised by a high-level switching logic. Methods for constructing such controller families have been discussed in the recent paper by the authors. The present paper concentrates on the switching task in a multiple model context. We describe and compare two different switching logics, and in each case study the behavior of the resulting closed-loop hybrid system.

110734. Linear Deductive Planning - Gerd Groe,Th Darmstadt,Steffen Holldobler Tu Dresden
Recently, three approaches to deductive planning were developed, which solve the technical frame problem without the need to state frame axioms explicitly. These approaches are based on the linear connection method, an equational Horn logic, and linear logic. At first glance these approaches seem to be very different. In the linear connection method a syntactical condition --- each literal is connected at most once --- is imposed on proofs. In the equational logic approach situations and plans are represented as terms and SLDE-resolution is applied as an inference rule. The linear logic approach is a Gentzen style proof system without...

110735. Coalgebras and Modal Logic - Colebrs Nd Modl Loi,Alexander Kurz
and Concrete Categories. John Wiley & Sons, 1990.

110736. On the Benefits of Rewrite Logic as a Semantics for Algebraic Petri Nets in Computing Siphons and Traps - Nasreddine Aoumeur,I Gunter Saake
A lot of research is being done to directly apply to high level nets structural techniques similar to those existing for place transition nets. In particular, the question of computing siphons for high level nets is of intrest since the well known results about relations between liveness of a net and control of its siphons. In this paper, we show how one can derive an efficient computing of siphons containing a given place from an appropriate interpretation of algebraic Petri nets in rewrite logic as a true concurrent semantics. Within this method, the verification procedure of symbolic siphons is reduced to two easy-understandable inference rewrite rules instead...

110737. A Correct, Precise and Efficient Integration of Set-Sharing, Freeness and Linearity for the Analysis of Finite and Rational Tree Languages - Patricia M. Hill,Enea Zaffanella,Roberto Bagnara
It is well-known that freehess and linearity information positively interact with aliasing information, therefore allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper we present a novel combination of set-sharing with freehess and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in [3] also applies to this abstract domain combination: this allows for the implementation of an abstract unification operator...

110738. Mirror Mirror In My Hand: a duality between specifications and models of process behaviour - J. L. Fiadeiro,J. F. Costa
Since Pnueli's seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes.

110739. Unknown - Riddle Of Induction
ts the fact that depending on the space of alternative hypotheses, means-ends analysis may select a different hypothesis on the same evidence: "all emeralds are green" in my Goodmanian Riddle, and "all emeralds are grue" in his. To my mind, his example proves that means-ends epistemology is not biased towards green-blue rather than grue-bleen. (A formal demonstration that means-ends analysis is language-invariant for all inductive problems appears in my paper "The Logic of Reliable and Efficient Inquiry" [Schulte 99].) Chart, however, concludes that "means-ends epistemology does not resolve Goodman's problem". That depends on what one takes Goodman's problem to be. If the problem is to find the...

110740. Tuning Of A Neuro-Fuzzy Controller By Genetic Algorithms With An Application To A Coupled-Tank Liquid-Level Control System - Teo Lian Seng,Marzuki Khalid,Rubiyah Yusof,Universiti Teknologi Malaysia
Fuzzy logic, neural networks and genetic algorithms are three popular artificial intelligence techniques that are widely used in many applications. Due to their distinct properties and advantages, they are currently being investigated and integrated to form new models or strategies in the areas of system control. In this paper, a neuro-fuzzy controller (referred to as NFCGA) based on the radial basis function neural network is tuned automatically using genetic algorithms (GA). A linear mapping method is used to encode the GA chromosome, which consists of the width and centre of the membership functions, and also the weights of the controller. Dynamic crossover and mutation probabilistic rates are...


Busque un recurso