Mostrando recursos 161 - 180 de 5.362

  1. Constructive Logics Part II: Linear Logic and Proof Nets

    Gallier, Jean H
    The purpose of this paper is to give an exposition of material dealing with constructive logics, typed λ-calculi, and linear logic. The first part of this paper gives an exposition of background material (with a few exceptions). This second part is devoted to linear logic and proof nets. Particular attention is given to the algebraic semantics (in Girard's terminology, phase semantics) of linear logic. We show how phase spaces arise as an instance of a Galois connection. We also give a direct proof of the correctness of the Danos-Regnier criterion for proof nets. This proof is based on a purely...

  2. Specifying Filler-Gap Dependency Parsers in a Linear-Logic Programming Language

    Hodas, Joshua S.
    An aspect of the Generalized Phrase Structure Grammar formalism proposed by Gazdar, et al. is the introduction of the notion of "slashed categories" to handle the parsing of structures, such as relative clauses, which involve unbounded dependencies. This has been implemented in Definite Clause Grammars through the technique of gap threading, in which a difference list of extracted noun phrases (gaps) is maintained. However, this technique is cumbersome, and can result in subtle soundness problems in the implemented grammars. Miller and Pareschi have proposed a method implementing gap threading at the logical level in intuitionistic logic. Unfortunately that implementation itself...

  3. Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language

    Felty, Amy; Miller, Dale
    Various forms of typed λ-calculi have been proposed as specification languages for representing wide varieties of object logics. The logical framework, LF, is an example of such a dependent-type λ-calculus. A small subset of intuitionistic logic with quantification over simply typed λ-calculus has also been proposed as a framework for specifying general logics. The logic of hereditary Harrop formulas with quantification at all non-predicate types, denoted here as hhω, is such a meta-logic that has been implemented in both the Isabelle theorem prover and the λProlog logic programming language. Both frameworks provide for specifications of logics in which details involved...

  4. Efficient Constraints on Possible Worlds for Reasoning About Necessity

    Stone, Matthew
    Modal logics offer natural, declarative representations for describing both the modular structure of logical specifications and the attitudes and behaviors of agents. The results of this paper further the goal of building practical, efficient reasoning systems using modal logics. The key problem in modal deduction is reasoning about the world in a model (or scope in a proof) at which an inference rule is applied - a potentially hard problem. This paper investigates the use of partial-order mechanisms to maintain constraints on the application of modal rules in proof search in restricted languages. The main result is a simple, incremental...

  5. Unification of Simply Typed Lambda-Terms as Logic Programming

    Miller, Dale
    The unification of simply typed λ-terms modulo the rules of ß- and η-conversions is often called "higher-order" unification because of the possible presence of variables of functional type. This kind of unification is undecidable in general and if unifiers exist, most general unifiers may not exist. In this paper, we show that such unification problems can be coded as a query of the logic programming language Lλ in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in Lλ the notions of equality and substitution of the simply typed λ-calculus: the rest of the unification...

  6. The Pi-Calculus as a Theory in Linear Logic: Preliminary Results

    Miller, Dale
    The agent expressions of the π-calculus can be translated into a theory of linear logic in such a way that the reflective and transitive closure of π-calculus (unlabeled) reduction is identified with "entailed-by". Under this translation, parallel composition is mapped to the multiplicative disjunct ("par") and restriction is mapped to universal quantification. Prefixing, non-deterministic choice (+), replication (!), and the match guard are all represented using non-logical constants, which are specified using a simple form of axiom, called here a process clause. These process clauses resemble Horn clauses except that they may have multiple conclusions; that is, their heads may...

  7. An Overview of Lambda-Prolog

    Nadathur, Gopalan; Miller, Dale
    λ-Prolog is a logic programming language that extends Prolog by incorporating notions of higher-order functions, λ-terms, higher-order unification, polymorphic types, and mechanisms for building modules and secure abstract data types. These new features are provided in a principled fashion by extending the classical first-order theory of Horn clauses to the intuitionistic higher-order theory of hereditary Harrop formulas. The justification for considering this extension a satisfactory logic programming language is provided through the proof-theoretic notion of a uniform proof. The correspondence between each extension to Prolog and the new features in the stronger logical theory is discussed. Also discussed are various...

  8. Deriving Mixed Evaluation From Standard Evaluation for a Simple Functional Language

    Hannan, John; Miller, Dale
    We demonstrate how a specification for the standard evaluation of a simple functional programming language can be systematically extended to a specification for mixed evaluation. Using techniques inspired by natural semantics we specify a standard evaluator by a set of inference rules. The evaluation of programs is then performed by a restricted kind of theorem proving in this logic. We then describe a systematic method for extending the proof system for standard evaluation to a new proof system that provides greater flexibility in treating bound variables in the object-level functional programs. We demonstrate how this extended proof system provides the...

  9. Extending Definite Clause Grammars With Scoping Constructs

    Pareschi, Remo; Miller, Dale
    Definite Clause Grammars (DCGs) have proved valuable to computational linguists since they can be used to specify phrase structured grammars. It is well known how to encode DCGs in Horn clauses. Some linguistic phenomena, such as filler-gap dependencies, are difficult to account for in a completely satisfactory way using simple phrase structured grammar. In the literature of logic grammars there have been several attempts to tackle this problem by making use of special arguments added to the DCG predicates corresponding to the grammatical symbols. In this paper we take a different line, in that we account for filler-gap dependencies by...

  10. Evidence-Based Audit, Technical Appendix

    Vaughan, Jeffrey A; Jia, Limin; Mazurak, Karl; Zdancewic, Stephan A
    Authorization logics provide a principled and flexible approach to specifying access control policies. One of their compelling benefits is that a proof in the logic is evidence that an access-control decision has been made in accordance with policy. Using such proofs for auditing reduces the trusted computing base and enables the ability to detect flaws in complex authorization policies. Moreover, the proof structure is itself useful, because proof normalization can yield information about the relevance of policy statements. Untrusted, but well-typed, applications that access resources through an appropriate interface must obey the access control policy and create proofs useful for...

  11. Lexical Scoping as Universal Quantification

    Miller, Dale
    A universally quantified goal can be interpreted intensionally, that is, the goal ∀x.G(x) succeeds if for some new constant c, the goal G(c) succeeds. The constant c is, in a sense, given a scope: it is introduced to solve this goal and is "discharged" after the goal succeeds or fails. This interpretation is similar to the interpretation of implicational goals: the goal D ⊃ G should succeed if when D is assumed, the goal G succeeds. The assumption D is discharged after G succeeds or fails. An interpreter for a logic programming language containing both universal quantifiers and implications in...

  12. Representing Objects in a Logic Programming Language With Scoping Constructs

    Hodas, Joshua S; Miller, Dale
    We present a logic programming language that uses implications and universal quantifiers in goals and in the bodies of clauses to provide a simple scoping mechanism for program clauses and constants. Within this language it is possible to define a simple notion of parametric module and local constant. Given this ability to structure programs, we explore how object-oriented programming, where objects are viewed as abstractions with behaviors, state, and inheritance, might be accommodated. To capture the notion of mutable state, we depart from the pure logic setting by adding a declaration that certain local predicates are deterministic (they succeed at...

  13. Logical and Computational Aspects of Programming With Sets/Bags/Lists

    Tannen, Val; Subrahmanyam, Ramesh
    We study issues that arise in programming with primitive recursion over non-free datatypes such as lists, bags and sets. Programs written in this style can lack a meaning in the sense that their outputs may be sensitive to the choice of input expression. We are, thus, naturally led to a set-theoretic denotational semantics with partial functions. We set up a logic for reasoning about the definedness of terms and a deterministic and terminating evaluator. The logic is shown to be sound in the model, and its recursion free fragment is shown to be complete for proving definedness of recursion free...

  14. Rigid E-Unification: NP-Completeness and Applications to Equational Matings

    Gallier, Jean H; Narendran, Paliath; Plaisted, David; Snyder, Wayne
    Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending Andrews's theorem proving method of matings to first-order languages with equality. This extension was first presented in Gallier, Raatz, and Snyder, where it was conjectured that rigid E-unification is decidable. In this paper, it is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order...

  15. Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract

    Hodas, Joshua S; Miller, Dale
    Logic programming languages based on fragments of intuitionistic logic have recently been developed and studied by several researchers. In such languages, implications are permitted in goals and in the bodies of clauses. Attempting to prove a goal of the form D ⊃ G in a context τ leads to an attempt to prove the goal G in the extended context τ ∪{D}. While an intuitionistic notion of context has many uses, it has turned out to be either too powerful or too limiting in several settings. We refine the intuitionistic notion of context by using a fragment of Girard's linear...

  16. An Open-Source and Declarative Approach Towards Teaching Large-Scale Networked Systems Programming

    Saeed, Taher; Gill, Harjot; Fei, Qiong; Zhang, Zhuoyao; Loo, Boon Thau
    This paper describes our experiences at the University of Pennsylvania in developing course projects for a large advanced undergraduate and first year graduate course in networked systems. Students work in teams to develop substantial networked systems programming projects (>10000 lines of code) using network simulator 3 (ns-3), an emerging open-source network simulator that is aimed at replacing the popular ns-2 simulator. Projects are developed in layers, where students build upon earlier assignments, first developing a protocol for Internet Protocol (IP) routing, followed by a distributed hash table (DHT) overlay network, and finally, a keyword-based search engine. One novelty of our...

  17. Hardware/Software Organization of a High Performance ATM Host Interface

    Traw, C. Brendan S; Smith, Jonathan M
    Concurrent increases in network bandwidths and processor speeds have created a performance bottleneck at the workstation-to-network host interface. This is especially true for BISDN networks where the fixed length ATM cell is mismatched with application requirements for data transfer; a successful hardware/software architecture will resolve such differences and offer high end-to-end performance. The solution we report carefully splits protocol processing functions into hardware and software implementations. The interface hardware is highly parallel and performs all per-cell functions with dedicated logic to maximize performance. Software provides support for the transfer of data between the interface and application memory, as well as the...

  18. Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi

    Gallier, Jean H
    The purpose of this paper is to give an exposition of material dealing with constructive logic, typed λ-calculi, and linear logic. The emergence in the past ten years of a coherent field of research often named "logic and computation" has had two major (and related) effects: firstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans from what is traditionally called theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some "old" concepts found in mathematical logic, like natural deduction, sequent calculus,...

  19. What's So Special About Kruskal's Theorem and the Ordinal To? A Survey of Some Results in Proof Theory

    Gallier, Jean H
    This paper consists primarily of a survey of results of Harvey Friedman about some proof theoretic aspects of various forms of Krusal's tree theorem, and in particular the connection with the ordinal Ƭo. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Veblen Hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to Kruskal, the "tree theorem", as well as a "finite miniaturization" of Kruskal's theorem due to Harvey Friedman. These...

  20. Coherence and Consistency in Domains (Extended Outline)

    Gunter, Carl A; Jung, Achim
    Almost all of the categories normally used as a mathematical foundation for denotational semantics satisfy a condition known as consistent completeness. The goal of this paper is to explore the possibility of using a different condition - that of coherence - which has its origins in topology and logic. In particular, we concentrate on those posets whose principal ideals are algebraic lattices and whose topologies are coherent. These form a cartesian closed category which has fixed points for domain equations. It is shown that a "universal domain" exists. Since the construction of this domain seems to be of general significance,...

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.