A New Correctness Criterion for Cyclic Proof Nets

We define proof nets for cyclic multiplicative linear logic as edge bi-coloured graphs. Our characterization is purely graph theoretical and works without further complication for proof nets with cuts, which are usually harder to handle in the non-commutative case. This also provides a new characterization of the proof nets for the Lambek calculus (with the empty sequence) which simply are a restriction on the formulas to be considered (which are asked to be intuitionistic).     

A linear algorithm for MLL proof net correctness and sequentialization

The paper presents in full detail the first linear algorithm given in the literature (Guerrini (1999) [6]) implementing proof structure correctness for multiplicative linear logic without units. The algorithm is essentially a reformulation of the Danos contractibility criterion in terms of a sort of unification. As for term unification, a direct implementation of the unification criterion leads to a quasi-linear algorithm. Linearity is obtained after observing that the disjoint-set union-find at the core of the unification criterion is a special case of union-find with a real linear time solution.     

Rewritings for Polarized Multiplicative and Exponential Proof Structures

We study conditions for a concurrent construction of proof-nets in the framework of linear logic following Andreoli's works. We define specific correctness criteria for that purpose. We first study the multiplicative case and show how the correctness criterion given by Danos and decidable in linear time, may be extended to closed modules (i.e. validity of polarized proof structures). We then study the exponential case and give a correctness criterion by means of a contraction relation that helps to discover frontiers of exponential boxes.     

A Static Analysis Method for a Classical Linear Logic Programming Language

In this paper, we propose a new static analysis method which is applicable for a classical linear logic programming language.Andreoli et al. proposed a static analysis method for the classical linear logic programming language LO, but their method did not cover multiplicative connectives which are important for a resource-sensitive feature of linear logic.Our method, in contrast, covers multiplicative conjunction in addition to multiplicative disjunction and linear implication. An abstract proof graph, an AND-OR graph representing all possible sequent proofs, is constructed from a given program and goal sequent. The graph can be repeatedly refined by propagating information to eliminate unprovable nodes from the graph.We applied our prototype analyzer for a sorting program written in Forum. The sorting program was improved about 1000 times faster than the ordinary program without analysis, for sorting 6 elements by using the analysis result.     

On abstract resource semantics and computability logic

We show that the uniform validity is equivalent to the non-uniform validity for Blass' semantics of [A. Blass, A game semantics for linear logic, Ann. Pure Appl. Logic 56 (1992) 183–220]. We present a shorter proof (than that of [G. Japaridze, The intuitionistic fragment of computability logic at the propositional level, Ann. Pure Appl. Logic 147 (3) (2007) 187–227]) of the completeness of the positive fragment of intuitionistic logic for this semantics, computability logic semantics, and the abstract resource semantics.     

Supporting Function Calls within PELCR

In [M. Pedicini and F. Quaglia. A parallel implementation for optimal lambda-calculus reduction PPDP '00: Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 3–14, ACM, 2000, M. Pedicini and F. Quaglia. PELCR: Parallel environment for optimal lambda-calculus reduction. CoRR, cs.LO/0407055, accepted for publication on TOCL, ACM, 2005], PELCR has been introduced as an implementation derived from the Geometry of Interaction in order to perform virtual reduction on parallel/distributed computing systems.In this paper we provide an extension of PELCR with computational effects based on directed virtual reduction [V. Danos, M. Pedicini, and L. Regnier. Directed virtual reductions. In M. Bezem D. van Dalen, editor, LNCS 1258, pages 76–88. EACSL, Springer Verlag, 1997], namely a restriction of virtual reduction [V. Danos and L. Regnier. Local and asynchronous beta-reduction (an analysis of Girard's EX-formula). LICS, pages 296–306. IEEE Computer Society Press, 1993], which is a particular way to compute the Geometry of Interaction [J.-Y. Girard. Geometry of interaction 1: Interpretation of system F. In R. Ferro, et al. editors Logic Colloquium '88, pages 221–260. North-Holland, 1989] in analogy with Lamping's optimal reduction [J. Lamping. An algorithm for optimal lambda calculus reduction. In Proc. of 17th Annual ACM Symposium on Principles of Programming Languages. ACM, San Francisco, California, pages 16–30, 1990]. Moreover, the proposed solution preserves scalability of the parallelism arising from local and asynchronous reduction as studied in [M. Pedicini and F. Quaglia. PELCR: Parallel environment for optimal lambda-calculus reduction. CoRR, cs.LO/0407055, accepted for publication on TOCL, ACM, 2005].     

Non-commutative logic III: focusing proofs

It is now well-established that the so-called focalization property plays a central role in the design of programming languages based on proof search, and more generally in the proof theory of linear logic. We present here a sequent calculus for non-commutative logic (NL) which enjoys the focalization property. In the multiplicative case, we give a focalized sequentialization theorem, and in the general case, we show that our focalized sequent calculus is equivalent to the original one by studying the permutabilities of rules for NL and showing that all permutabilities of linear logic involved in focalization can be lifted to NL permutabilities. These results are based on a study of the partitions of partially ordered sets modulo entropy.     

Modeling and Verifying Graph Transformations in Proof Assistants

This paper takes first steps towards a formalization of graph transformations in a general setting of interactive theorem provers, which will form the basis for proofs of correctness of graph transformation systems. Whereas graph rewriting is usually performed by mapping a pattern graph into a source graph by means of a graph morphism and then carrying out operations on the image node and edge set, this article generalises the notion of pattern graph to path expressions, which are formulae in a fragment of first-order logic. We examine the correspondence with traditional graph rewriting and show that this interpretation is beneficial when formally reasoning about model transformations with the aid of proof assistants.     

Characterizing proximity trees

Complete characterizations are given for those trees that can be drawn as either the relative neighborhood graph, relatively closest graph, Gabriel graph, or modified Gabriel graph of a set of points in the plane. The characterizations give rise to linear-time algorithms for determining whether a tree has such a drawing; if such a drawing exists one can be constructed in linear time in the real RAM model. The characterization of Gabriel graphs settles several conjectures of Matula and Sokal [17].This research was conducted while the author was at the School of Computer Science of McGill University. Research supported in part by NSERC and FCAR.This work was done when this author was visiting the School of Computer Science of McGill University.This work was done when this author was visiting the School of Computer Science of McGill University.     

Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Avoiding deadlock is crucial to interconnection networks. In ’87, Dally and Seitz proposed a necessary and sufficient condition for deadlock-free routing. This condition states that a routing function is deadlock-free if and only if its channel dependency graph is acyclic. We formally define and prove a slightly different condition from which the original condition of Dally and Seitz can be derived. Dally and Seitz prove that a deadlock situation induces cyclic dependencies by reductio ad absurdum. In contrast we introduce the notion of a waiting graph from which we explicitly construct a cyclic dependency from a deadlock situation. Moreover, our proof is structured in such a way that it only depends on a small set of proof obligations associated to arbitrary routing functions and switching policies. Discharging these proof obligations is sufficient to instantiate our condition for deadlock-free routing on particular networks. Our condition and its proof have been formalized using the ACL2 theorem proving system.     

On the equivalence and range of applicability of graph-based representations of logic programs

Logic programs under Answer Sets semantics can be studied, and actual computation can be carried out, by means of representing them by directed graphs. Several reductions of logic programs to directed graphs are now available. We compare our proposed representation, called Extended Dependency Graph, to the Block Graph representation recently defined by Linke [Proc. IJCAI-2001, 2001, pp. 641-648]. On the relevant fragment of well-founded irreducible programs, extended dependency and block graph turns out to be isomorphic. So, we argue that graph representation of general logic programs should be abandoned in favor of graph representation of well-founded irreducible programs, which are more concise, more uniform in structure while being equally expressive.     

Syllogisms in Rudimentary Linear Logic, Diagrammatically

We present a reading of the traditional syllogistics in a fragment of the propositional intuitionistic multiplicative linear logic and prove that with respect to a diagrammatic logical calculus that we introduced in a previous paper, a syllogism is provable in such a fragment if and only if it is diagrammatically provable. We extend this result to syllogistics with complemented terms à la De Morgan, with respect to a suitable extension of the diagrammatic reasoning system for the traditional case and a corresponding reading of such De Morgan style syllogistics in the previously referred to fragment of linear logic.     

A Linear-Time Algorithm for Star-Shaped Drawings of Planar Graphs with the Minimum Number of Concave Corners

A star-shaped drawing of a graph is a straight-line drawing such that each inner facial cycle is drawn as a star-shaped polygon, and the outer facial cycle is drawn as a convex polygon. In this paper, we consider the problem of finding a star-shaped drawing of a biconnected planar graph with the minimum number of concave corners. We first show new structural properties of planar graphs to derive a lower bound on the number of concave corners. Based on the lower bound, we prove that the problem can be solved in linear time by presenting a linear-time algorithm for finding a best plane embedding of a biconnected planar graph with the minimum number of concave corners. This is in spite of the fact that a biconnected planar graph may have an exponential number of different plane embeddings.     

Extremal states on bounded residuated \ell-monoids with general comparability

Bounded residuated lattice ordered monoids (RlR\ell-monoids) are a common generalization of pseudo-BLBL-algebras and Heyting algebras, i.e. algebras of the non-commutative basic fuzzy logic (and consequently of the basic fuzzy logic, the Łukasiewicz logic and the non-commutative Łukasiewicz logic) and the intuitionistic logic, respectively. We investigate bounded RlR\ell-monoids satisfying the general comparability condition in connection with their states (analogues of probability measures). It is shown that if an extremal state on Boolean elements fulfils a simple condition, then it can be uniquely extended to an extremal state on the RlR\ell-monoid, and that if every extremal state satisfies this condition, then the RlR\ell-monoid is a pseudo-BLBL-algebra.     

Very and more or less in non-commutative fuzzy logic

In this paper we consider fuzzy subsets of a universe as L-fuzzy subsets instead of [ 0, 1 ]-valued, where L is a complete lattice. We enrich the lattice L by adding some suitable operations to make it into a pseudo-BL algebra. Since BL algebras are main frameworks of fuzzy logic, we propose to consider the non-commutative BL-algebras which are more natural for modeling the fuzzy notions. Based on reasoning with in non-commutative fuzzy logic we model the linguistic modifiers such as very and more or less and give an appropriate membership function for each one by taking into account the context of the given fuzzy notion by means of resemblance L-fuzzy relations.     

Application of Attribute NCE Graph Grammars to Syntactic Editing of Tabular Forms

In this paper, we deal with editing tabular forms for program specifications based on a particular graph grammar HNGG [2]. First, we formalize syntax-directed editing methods by extending of the notion of the Cornell Program Synthesizer [8] to attribute NCE graph grammars (cf. [1]). Next, we discuss the algorithms of the editing methods.     

Characterizing and recognizing the visibility graph of a funnel-shaped polygon

A funnel, which is notable for its fundamental role in visibility algorithms, is defined as a polygon that has exactly three convex vertices, two of which are connected by a boundary edge. In this paper we investigate the visibility graph of a funnel which we call an F-graph.We first present two characterizations of an F-graph, one of whose sufficiency proof itself is a linear time Real RAM algorithm for drawing a funnel on the plane that corresponds to an F-graph. We next give a linear-time algorithm for recognizing an F-graph. When the algorithm recognizes an F-graph, it also reports one of the Hamiltonian cycles defining the boundary of its corresponding funnel. This recognition algorithm takes linear time even on a RAM.We finally show that an F-graph is weakly triangulated and therefore perfect, which agrees with the fact that perfect graphs are related to geometric structures.This work was supported in part by the Korea Science and Engineering Foundation under Grant 91-01-01.     

Encoding Linear Logic with Interaction Combinators

The purpose of this paper is to demonstrate how Lafont's interaction combinators, a system of three symbols and six interaction rules, can be used to encode linear logic. Specifically, we give a translation of the multiplicative, exponential, and additive fragments of linear logic together with a strategy for cut-elimination which can be faithfully simulated. Finally, we show briefly how this encoding can be used for evaluating λ-terms. In addition to offering a very simple, perhaps the simplest, system of rewriting for linear logic and the λ-calculus, the interaction net implementation that we present has been shown by experimental testing to offer a good level of sharing in terms of the number of cut-elimination steps (resp. β-reduction steps). In particular it performs better than all extant finite systems of interaction nets.     

A theory for the derivation of combinational C-mos circuit designs

This paper shows how propositional logic may be used to reason about synchronous combinational switching circuits implemented in C-mos. It develops a simple formalism and theory for describing and predicting their behaviour. On this it builds a calculus of design which is driven by proof obligations. The design philosophy for software introduced in [1] is thereby extended to a certain kind of hardware design. No prior knowledge of hardware is assumed of the reader; but useful background, motivation, examples and pictures may be found in [2]. Many of the problems described in that paper have been solved in this one.     

Generalized Model-Checking over Locally Tree-Decomposable Classes

It has been proved in Frick and Grohe that properties of graphs or other relational structures that are definable in first-order logic can be decided in linear time when the input structures are restricted to come from a {\em locally tree-decomposable} class of structures. Important examples of such classes are the class of planar graphs and classes of graphs of bounded degree. In this paper we consider more general computational problems than decision problems, which are induced by formulas with free variables. In this generalized setting we investigate the construction (find a satisfying assignment), listing (all satisfying assignments) and counting (compute the number of satisfying assignments) problems for formulas of first-order logic. We show that each of these problems can be solved in linear time on locally tree-decomposable classes of structures. For instance, we devise an algorithm that, given a planar graph $\cal G$ and a first-order logic formula $\phi(\barx)$, computes a $\bara \in G$ such that $\cal G \models \phi(\bara)$ in time $f(||\phi||) \cdot ||\cal G||$ for some computable function $f$ (the construction case). Accordingly, we obtain linear time algorithms for the counting and listing cases.