Mostrando recursos 110.721 - 110.740 de 188.641

  1. ACL2: An Industrial Strength Version of Nqthm

    Matt Kaufmann; J. Strother Moore
    ACL2 is a reimplemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. However, the logic supported by ACL2 is compatible with the applicative subset of Common Lisp. The decision to use an "industrial strength" programming language as the foundation of the mathematical logic is crucial to our advocacy of ACL2 in the application of formal methods to large systems. However, one of the key reasons Nqthm has been so successful, we believe, is its insistence that functions be total. Common Lisp functions are not total and this is one of the reasons...

  2. Capturing Complexity Classes with Lindström Quantifiers

    J.A. Makowsky; Lindstrom Logics
    . We report on our efforts of unifying Descriptive Complexity Theory and Logic in the framework of axiomatic definitions of both Logics and Complexity Classes. (Joint work with Y.B. Pnueli) In the last 20 years several logics were exhibited which capture complexity classes such as L (LogSpace), NL (Non--deterministic LogSpace), P (Polynomial Time), NP (Non--deterministic Polynomial Time), PH (the polynomial hierarchy) , [Fag74, Imm87, Imm89, Sto87, Ste91]. In mathematical logic the theory of abstract model theory and Lindstrom quantifiers is well established [BF85]. In this talk we report our work concerning unification of Descriptive Complexity Theory and Abstract Model Theory....

  3. A Polymorphic Groundness Analysis of Logic Programs

    Lunjin Lu
    . A polymorphic analysis is an analysis whose input and output contain parameters which serve as placeholders for information that is unknown before analysis but provided after analysis. In this paper, we present a polymorphic groundness analysis that infers parameterised groundness descriptions of the variables of interest at a program point. The polymorphic groundness analysis is designed by replacing two primitive operators used in a monomorphic groundness analysis and is shown to be as precise as the monomorphic groundness analysis for any possible values for mode parameters. Experimental results of a prototype implementation of the polymorphic groundness analysis are given....

  4. Buffer Minimization in Pass Transistor Logic

    Hai Zhou; Adnan Aziz
    With the shrinking feature sizes and increasing transistor counts on chips, the push for higher speed and lower power makes it necessary to look for alternative design styles which offer better performance characteristics to static CMOS. Among them, pass transistor logic (PTL) circuits give great promise. Since the delay in a pass-transistor chain is quadratically proportional to the number of stages, and a signal may degenerate when passing through a transistor, buffers are necessary to guarantee performance and restore signal strength in PTL circuits. In this paper, we first analyze the effects of buffer insertion on a circuit and give...

  5. Coherence for Sharing Proof-nets

    Stefano Guerrini; Stefano Guerrini; Simone Masini; Simone Martini; Andrea Masini; Andrea Masini
    this paper is a solution to the coherence problem (for restricted proof-nets, see below) obtained by changing the way the information is coded into sharing graphs. This is achieved via two technical tools: (i) a new reduction rule (absorption) allowing a simplification of the net in some critical cases; (ii) a clear separation of the logical and control information in the representation of a net. The logical information takes the form of levels on the formulas of the proof-net; control is expressed by unifying fans and brackets into one single node (mux ). It is this separation to allow the...

  6. Lectures on Proof Theory

    Samuel Buss; A. Maciel (mcgill; E. Allender (rutgers; P. Mckenzie
    proof systems ffl Extended Frege (eF) and substitution Frege (sF) systems ffl Tautologies based on the Pigeon-Hole Principle (PHP) ffl Best-known lower bounds, including a survey of the state of the art for bounds on proof lengths in various restricted fragments of Frege systems For all of this work, we will use propositional formulas, which are built up out of the following: ffl Variables: p 1 ; p 2 ; p 3 ; : : :; or informally, p; q; r; : : : ffl Logical connectives: :, , , !, $, \Phi ,: : : . We will talk...

  7. A Predictive Bottom-up Evaluator

    Manuel Vilares; Manuel Vilares Ferro; Miguel Angel; Alonso Pardo
    This paper 1 presents a recursive query processing strategy on Horn Clauses which plays, with respect to classic context-free parsing algorithms, a similar role to the well known LALR compilation schemes. Over a base structure equipped with an efficient context-free parsing algorithm based on dynamic programming techniques, we define a logic push-down automaton which breaks computations into combinable, sharable and storable sub-computations. The latter provides computation sharing and operational completeness and solves most of the problems posed by classic depth-first left-to-right traversals. 1 Introduction Context-free parsing represents a fine starting point to understand computational aspects of syntactic phenomena in full...

  8. Possibility Measures, Random Sets And Natural Extension

    Gert De; Gert de Cooman; Dirk Aeyels
    . We study the relationship between possibility and necessity measures defined on arbitrary spaces, the theory of imprecise probabilities, and elementary random set theory. We show how special random sets can be used to generate normal possibility and necessity measures, as well as their natural extensions. This leads to interesting alternative formulas for the calculation of these natural extensions. 1. Introduction Possibility measures were introduced by Zadeh [21] in 1978. In his view, these supremum preserving set functions are a mathematical representation of the information conveyed by typical affirmative statements in natural language. For recent discussions of this interpretation, we...

  9. Type Analysis for CHIP

    Wlodzimierz Drabent; Pawel Pietrzak
    The paper presents a proposal for type analysis for CLP languages and shows its application to the CHIP language. Our approach is based on descriptive types and adopts some techniques developed for LP. We are mainly interested in types approximating operational semantics, given by the set of procedure calls and successes that appear during computations. We also consider approximating the declarative semantics. The types dealt with in this work are sets of constrained terms. This makes it possible to express groundness information. We use c-semantics as the declarative semantics. To deal with operational semantics we use its characterization by the...

  10. Selecting Behaviors using Fuzzy Logic

    Francois Michaud
    Behavior-based systems, i.e. systems that use behaviors as a way of decomposing the control policy needed for accomplishing a task, are very useful in making robots cope with the dynamics of real-world environments. However, these systems still need to be extended to design robots having multiple and possibly conflicting goals, requiring planning, and getting more out of their behaviors. One way of doing that is to allow behaviors to be selected dynamically and to blend their actions in order to get more complex behaviors. This paper addresses these issues by presenting a control architecture that, when using fuzzy logic, allows...

  11. A Study Of Variants Of The Lambek Calculus And An Implementation In Prolog

    D. Stott Parker; Parker Csd; Shen-tzay Huang; D. Stott Parker
    A framework for types of logic programs, in particular, those embodying lazy computation and infinite objects, is proposed. Examples are given to illustrate the need. Starting with two methodological views, Types As Sets (subsets of the Herbrand Universe) and Types for The Prolog Computational Model, we give a simple monomorphic type structure and extend it with principles of polymorphismand homogeneity. The SVP model of Parker, Simon and Valduriez is given a detailed type analysis as an application of this framework. Common logic programs serve as other instances of application. Directions for enriching the type structure (Herbrand Type Universe) are discussed....

  12. Free Variable Tableaux for a Many Sorted Logic with Preorders

    Antonio Gavilanes; Javier Leach; Susana Nieva; A. Gavilanes; J. Leach; S. Nieva
    The proof of properties of formal systems including inequalities is currently evolving into an increasingly appealing workline in different areas of computer science. We propose a sound and complete semantic tableau method for handling many-sorted preorders. As logical framework a many-sorted first order logic is supplied, where functions and predicates behave monotonically or antimonotonically on their arguments. We formulate additional expansion tableau rules as a more efficient alternative to adding the axioms characterizing a preordered structure. Efficiency of the method is improved using a free variable tableau version. Completeness of the system is proved in detail; examples and applications are...

  13. Integrating EBL and ILP to Acquire Control Rules for Planning

    Tara Estlin; Raymond J. Mooney
    Most approaches to learning control information in planning systems use explanation-based learning to generate control rules. Unfortunately, EBL alone often produces overly complex rules that actually decrease planning efficiency. This paper presents a novel learning approach for control knowledge acquisition that integrates explanation-based learning with techniques from inductive logic programming. EBL is used to constrain an inductive search for selection heuristics that help a planner choose between competing plan refinements. Scope is one of the few systems to address learning control information in the newer partial-order planners. Specifically, Scope learns domain-specific control rules for a version of the UCPOP planning...

  14. Rewriting Systems

    Lecture Notes; Johan Boye; Ulf Nilsson
    reduction systems . . . . . . . . . . . . . . . . . . . . 15 1.6 Properties of arss . . . . . . . . . . . . . . . . . . . . . . . . . 16 2 Lambda calculus and combinatory logic 21 2.1 Lambda terms . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.2 The rewrite rules . . . . ....

  15. Deductive and Active Databases: Two Paradigms or Ends of a Spectrum?

    Jennifer Widom
    This position paper considers several existing relational database rule languages with a focus on exploring the fundamental differences between deductive and active databases. We find that deductive and active databases do not form two discernible classes, but rather they delineate two ends of a spectrum of database rule languages. We claim that this spectrum also corresponds to a notion of abstraction level, with deductive rule languages at a higher level and active rule languages at a lower level. 1 Introduction Research on incorporating rule processing into database systems historically has been divided into two distinct areas: deductive databases and active...

  16. Database Query Languages Embedded in the Typed Lambda Calculus

    Gerd G. Hillebrand; Paris C. Kanellakis; Harry G. Mairson
    We investigate the expressive power of the typed -calculus when expressing computations over finite structures, i.e., databases. We show that the simply typed -calculus can express various database query languages such as the relational algebra, fixpoint logic, and the complex object algebra. In our embeddings, inputs and outputs are -terms encoding databases, and a program expressing a query is a -term which types when applied to an input and reduces to an output. Our embeddings have the additional property that PTIME computable queries are expressible by programs that, when applied to an input, reduce to an output in a PTIME...

  17. Concurrent Constraint Programming and Non-Commutative Logic

    Paul Ruet; François Fages
    . This paper presents a connection between the intuitionistic fragment of a non-commutative version of linear logic introduced by the first author (NLI) and concurrent constraint programming (CC). We refine existing logical characterizations of operational aspects of CC, by providing a logical interpretation of finer observable properties of CC programs, namely stores, successes and suspensions. 1 Introduction The class CC(X ) of Concurrent Constraint programming languages introduced by Saraswat [29] in 1987 arises as a natural combination of constraint logic programming [11] and concurrent logic programming, with a synchronization mechanism based on constraint entailment [16]. CC programming is a model...

  18. Deductive Verification of Real-time Systems Using STeP

    Nikolaj S. Bjørner; Zohar Manna; Henny B. Sipma; Tomás E. Uribe; Tom'as E. Uribe
    . We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logic. We show how deductive verification rules, verification diagrams, and automatic invariant generation can be used to establish properties of real-time systems in this framework. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP. 1 Introduction The formalism of clocked transition systems was introduced by Manna and Pnueli [MP96] as a simple model for real-time systems. Continuous real-time is modeled explicitly as part of the system, in...

  19. Fuzzy Controller for Obstacle-Avoidance With a Non-Holonomous Mobile Robot

    Juan Pedro Uribe
    This paper describes the design and development of a sensor based navigation system which makes it possible for a non-holonomous mobile robot to avoid obstacles using information on its environment picked up by a belt of ultrasonic sensors. To control the robot no preliminary information regarding its environment is required, the robot adapts to them through the information gathered on the spot by the ultrasonic sensors and the information released from a spatial memory. The controller allows the generation of the signal to the robot's motors, it has been developed based on the concept of general perception, and the principles...

  20. Classes Of Byzantine Fault-Tolerant Algorithms For Dependable Distributed Systems

    André Postma; Andr� Postma; Andr� Postma
    1 1.1. Dependable computer systems 1 1.1.1. Dependability attributes 2 1.1.2. The impairments to dependability 3 1.1.2.1. Faults, errors, and failures 3 1.1.2.2. Fault and failure classification 3 1.1.3. Dependability measures 5 1.1.4. The means of dependability 7 1.1.5. Overview 11 1.2. Fault detection techniques 11 1.2.1. Duplication 11 1.2.2. Error-detecting codes 12 1.2.3. Checksums 12 1.2.4. Self-checking and fail-safe logic 12 1.2.5. Watch-dog timers and bus timeouts 13 1.2.6. Consistency and capability checks 13 1.2.7. Processor monitoring 14 1.2.8. Program monitoring 14 1.3. Fault-tolerance techniques 14 1.3.1. Masking redundancy techniques 15 1.3.1.1. N-modular redundancy 15 1.3.1.2. Error-correcting codes 16...

Aviso de cookies: Usamos cookies propias y de terceros para mejorar nuestros servicios, para análisis estadístico y para mostrarle publicidad. Si continua navegando consideramos que acepta su uso en los términos establecidos en la Política de cookies.