Sunday, September 21, 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 132,413

110721. Compiling Systemic Grammar into Feature Logic Systems - Renate Henschel
this paper is, therefore, to re-represent systemic grammar resources in a standard typed feature logic in order (1) to clarify theoretically the relation between systemic grammar and state-of-the-art feature logics, and (2) to serve as point of departure for bidirectional processing of systemic grammar. Four such representations in the feature logic formalisms ale, tfs, cuf and tdl

110722. GOLEX --- Bridging the Gap between Logic (GOLOG) and a Real Robot - Dirk Hahnel,Wolfram Burgard,Gerhard Lakemeyer
. The control of mobile robots acting autonomously in the real world is one of the long-term goals of the field of artificial intelligence. So far the field lacks methods bridging the gap between the sophisticated symbolic techniques to represent and reason about action and more and more reliable low-level robot control and navigation systems. In this paper we present GOLEX, an execution and monitoring system for the logic-based action language GOLOG and the complex and distributed RHINO control software which operates on RWI B21 and B14 mobile robots. GOLEX provides the following features: it maps abstract primitive actions into low-level commands of the robot control system,...

110723. Jinni: Intelligent Mobile Agent Programming at the Intersection of Java and Prolog - Paul Tarau
. Jinni (Java INference engine and Networked Interactor), is a lightweight, multi-threaded, logic programming language, intended to be used as a flexible scripting tool for gluing together knowledge processing components and Java objects in distributed applications. Jinni threads are coordinated through blackboards, local to each process. Associative search based on term unification (a variant of Linda) is used as the basic synchronization mechanism. Threads are controlled with tiny interpreters following a scripting language based on a subset of Prolog. Mobile threads, implemented by capturing first order continuations in a compact data structure sent over the network, allow Jinni to interoperate with remote high performance BinProlog servers for CPU-intensive knowledge processing and...

110724. STDL A Portable Language for Transaction Processing - Philip A. Bernstein,Per O. Gyllstrom,Tom Wimberg
This paper describes STDL's transaction features: transaction bracketing, transactional remote procedure call, transactional queuing, recoverable terminal I/O, and transactional exception handling. STDL relies on standard C and COBOL for most application logic and all operations on SQL databases and files. All transactional features of STDL and new features outside standard C and COBOL are isolated in procedures written in the STDL language. These procedures are called tasks. This isolation of transactional features is quite different than other persistent programming languages: one can use applications written in standard C or COBOL; and to implement STDL, it is possible to map clauses of task language onto operations of most any distributed TP monitor. Keywords: transactions,...

110725. Design of Experiments in CAD: Context and New Data Sets for ISCAS'99 - Franc Brglez,Rolf Drechsler
This paper introduces the background and motivation for the two special sessions at ISCAS'99. The sessions bring together eight papers, each rooted in the methodology of experimental design, and contributed by collaborating teams of distributed participants. The paper briefly outlines the premises of the companion papers that follow, provides a brief description of a typical experimental design, and introduces a design for archival of data sets and results that are to be readily accessible on the Web. Keywords: design of experiments, circuit equivalence classes, benchmarking. 1 Introduction More than a thousand mathematical problems arising in engineering and science have been shown to be NP-hard. Data sets such as ISCAS'85, ISCAS'89, and extensions introduced at logic...

110726. Intellectual Property Protection By Watermarking Combinational Logic Synthesis Solutions - Darko Kirovski,Yean-yow Hwang,Miodrag Potkonjak,Jason Cong
The intellectual property (IP) business model is vulnerable to a number of potentially devastating obstructions, such as misappropriation and intellectual property fraud. We propose a new method for IP protection (IPP) which facilitates design watermarking at the combinational logic synthesis level. We developed protocols for embedding designer- and/or tool-specific information into a logic network while performing multi-level logic minimization and technology mapping. We demonstrate that the difficulty of erasing author 's signature or finding another signature in the synthesized design can be made arbitrarily computationally difficult. We also developed a statistical method which enables us to establish the strength of the proof of authorship. The watermarking method has been tested on a...

110727. Efficiently Supporting Fault-Tolerance in FPGAs - John Lach,William H. Mangione-smith,Miodrag Potkonjak
While system reliability is conventionally achieved through component replication, we have developed a fault-tolerance approach for FPGA-based systems that comes at a reduced cost in terms of design time, volume, and weight. We partition the physical design into a set of tiles. In response to a component failure, we capitalize on the unique reconfiguration capabilities of FPGAs and replace the affected tile with a functionally equivalent tile that does not rely on the faulty component. Unlike fixed structure faulttolerance techniques for ASICs and microprocessors, this approach allows a single physical component to provide redundant backup for several types of components. Experimental results conducted on a subset of the MCNC benchmarks demonstrate a high level of reliability with low...

110728. A Hybrid Backward Slicing Algorithm Producing Executable Slices for Prolog - Campus Universitaire De Beaulieu
ion of a literal) An abstraction of a literal A is the literal A where zero, one or more arguments have been replaced by anonymous variables. Definition 3 (Abstraction of a clause) If C is the clause A / B 1 ; : : : ; Bn , an abstraction of C is either: ffl the empty clause, denoted by ;, or ffl a unit clause, denoted by A 0 /, where A 0 is an abstraction of A, or ffl a clause of the form A 0 / B 0 1 ; : : : ; B 0 p , derived from C by removing zero, one or more literals of the body and where all...

110729. STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems - Tom'as E. Uribe,Anca Browne,Eddie Chang,Arjun Kapur,Zohar Manna,Henny B. Sipma
. The Stanford Temporal Prover, STeP, combines deductive methods with algorithmic techniques to verify linear-time temporal logic specifications of reactive and real-time systems. STeP uses verification rules, verification diagrams, automatically generated invariants, model checking, and a collection of decision procedures to verify finite- and infinite-state systems. System Description: The Stanford Temporal Prover, STeP, supports the computer-aided formal verification of reactive, real-time (and, in particular, concurrent) systems based on temporal specifications. Reactive systems maintain an ongoing interaction with their environment; their specifications are typically expressed as constraints on their behavior over time. STeP is not restricted to finite-state systems, but combines algorithmic and deductive methods to allow the verification of a broad class...

110730. Proof-terms for classical and intuitionistic resolution (Extended Abstract) - Eike Ritter,David Pym,Lincoln Wallen
. We exploit a system of realizers for classical logic, and a translation from resolution into the sequent calculus, to assess the intuitionistic force of classical resolution for a fragment of intuitionistic logic. This approach is in contrast to formulating locally intuitionistically sound resolution rules. The techniques use the ¯ffl-calculus, a development of Parigot's ¯-calculus. 1 Introduction 1.1 Local methods for intuitionistic logic It is standard practice to draw a sharp distinction between local methods of automated deduction for classical logic, inspired by techniques such as Robinson 's resolution [17] and Maslov's inverse method [9], and global methods, those inspired by Gentzen's sequent calculus [8] and Smullyan's tableaux systems [18]. For a...

110731. Deriving Logic Programs From Observations - David Gilbert,Christopher Hogger
This paper describes a method for deriving logic programs from observations that can be made of the progress of a computation. Such observations can be regarded as extrinsic specifications, and can be represented as directed acyclic graphs. Each computation that the system can perform is represented by a path through the graph which in turn can be described in first order logic. Logic programs can be derived from these first order logic descriptions by standard transformations. In this paper we chose to derive sequential logic programs, but the method is equally applicable to concurrent systems. Introduction A logic programming system can be viewed as a black box for...

110732. A Spatio-Temporal Logic for 2D Multi-Agent Problem Domains - Wanlin Pang
We formally present a first order logic intended for representing and reasoning about 2D dynamic multiagent problem domains. The unique feature of the logic is the uniform use of a Cartesian plane as the basis for both the spatial and temporal ontology. Our temporal structure has an ever changing present. Relative to each present there is a past and a future. A feature of this temporal structure is its ability to capture when knowledge is added or updated. 1 Introduction One important facet of Distributed Artificial Intelligence (DAI) is the composition of groups of agents at different social levels: groups, organizations, etc. [?]. A requirement is the...

110733. Default Logic and Autoepistemic Logic: Fixed Points and Common Semantic Framework - Choh Man Teng
When we work with information from multiple sources, the formats of the knowledge bases may not be uniform. It would be desirable to be able to combine a knowledge base of default rules with one containing autoepistemic formulas. Previous works on relating default logic and autoepistemic logic mostly impose some constraints on autoepistemic logic, and thus are not suitable for combining the two logics. We first present a fixed point formulation of autoepistemic logic analogous to that of default logic. Then we introduce a possible world framework with a partition structure, which corresponds to our intuitive notion of accessibility as linking alternate "possible" worlds. We show that...

110734. An Institution of Object Behaviour - Jos Félix Costa
. An institution for a simple logic of behaviour is built using a cofibration from a category of transition systems into the envisaged category of signatures. The chosen propositional, linear temporal logic distinguishes between event occurrence and event enabling. The satisfaction condition is proved using a fibered adjunction between transition systems and their computations. The operational semantics of behaviour specifications is briefly discussed. 1 Introduction Consolidating the conjectures in [SernadasA et al 92a], we study the problem of setting-up a suitable institution (see [Goguen and Burstall 84]) of linear temporal logic from a given reasonable semantic domain of object behaviour. For the sake of simplicity we work towards a propositional fragment. No...

110735. A Combinator-based Order-sorted Higher-order Unification Algorithm - Patricia Johann,Fachbereich Informatik
This paper develops a sound and complete transformation-based algorithm for unification in an extensional order-sorted combinatory logic supporting constant overloading and a higher-order sort concept. Appropriate notions of order-sorted weak equality and extensionality --- reflecting order-sorted fij-equality in the corresponding lambda calculus given by Johann and Kohlhase --- are defined, and the typed combinator-based higher-order unification techniques of Dougherty are modified to accommodate unification with respect to the theory they generate. The algorithm presented here can thus be viewed as a combinatory logic counterpart to that of Johann and Kohlhase, as well as a refinement of that of Dougherty, and provides evidence that combinatory logic is well-suited to serve...

110736. Multi Lingual Sequent Calculus and Coherent Spaces - Achim Jung,Mathias Kegelmann,M. Andrew Moshier
We study a Gentzen style sequent calculus where the formulas on the left and right of the turnstile need not necessarily come from the same logical system. Such a sequent can be seen as a consequence between different domains of reasoning. We discuss the ingredients needed to set up the logic generalized in this fashion. The usual cut rule does not make sense for sequents which connect different logical systems because it mixes formulas from antecedent and succedent. We propose a different cut rule which addresses this problem. The new cut rule can be used as a basis for composition in a suitable category of logical systems. As...

110737. A Reliable Mobile Agents Architecture - Manfred Dalmeijer,Eric Rietjens,Michiel Soede,D. K. Hammer,A. T. M. Aerts
This paper describes the design of a novel mobile agent system that supports the flexible and reliable interaction of autonomous components in an object-oriented distributed system. It discusses the object-oriented design of the overall system together with a number of important components in terms of the most important design decisions. A detailed description of the reliability model is given in terms of the failure hypothesis and the related recovery protocols. Special emphasis is given to the generality and efficiency of the implementation and a number of preliminary experiences are described. 1. Introduction This paper focuses on the design and implementation of an object oriented mobile agent system. A mobile...

110738. Sequential Implementation of Parallel Narrowing
Parallel Narrowing is a narrowing strategy which exploits expression parallelism. We present the ørst implementation by transforming weakly orthogonal, constructor-based programs into Prolog with the help of parallel deønitional trees. We deøne translation scheme for the general case of multistep narrowing, which is then extended to parallel narrowing by additional elimination rules. Our implementation is improved by combining parallel narrowing with intermediate simpliøcation steps. Advantages of the new strategies and speciøc challenges of a Prolog implementation are pointed out by comparative measurements. 1 Introduction Functional logic languages combine the advantages of functional languages, such as higher order functions and eOEcient evaluation with those of logic languages like search, logical...

110739. A Survey of Categorical Computation: Fixed Points, . . .
Machine by Curien [Cur86]. It is based upon a weak categorical combinatory logic, viz. lacking surjective pairing and extensionality, that arose as a direct semantic-to-syntactic translation of the lambda calculus of tuples. The computational mode was combinator term reduction through rewriting using a direct left-to-right parse algorithm, initially making the evaluation strategy inefficiently eager 1 . Application is therefore simply juxtaposition, losing the full expressiveness of-reduction that computes via substitution. Its overly strong bias towards the lambda calculus was another factor that limited its expressiveness. On one hand the CAM demanded the existence of categorical products but on the other it had no coproducts for developing many useful data structures....

110740. Definability and Descriptive Complexity on Databases of Bounded Tree-Width - Martin Grohe,Julian Marino
. We study the expressive power of various query languages on relational databases of bounded tree-width. Our first theorem says that fixed-point logic with counting captures polynomial time on classes of databases of bounded tree-width. This result should be seen on the background of an important open question of Chandra and Harel [7] asking whether there is a query language capturing polynomial time on unordered databases. Our theorem is a further step in a larger project of extending the scope of databases on which polynomial time can be captured by reasonable query languages. We then prove a general definability theorem stating that each query on a class of databases...

 

Busque un recurso