A game semantics for disjunctive logic programming

Denotational semantics of logic programming and its extensions (by allowing negation, disjunctions, or both) have been studied thoroughly for many years. In 1998, a game semantics was given to definite logic programs by Di Cosmo, Loddo, and Nicolet, and a few years later it was extended to deal with negation by Rondogiannis and Wadge. Both approaches were proven equivalent to the traditional semantics. In this paper we define a game semantics for disjunctive logic programs and prove soundness and completeness with respect to the minimal model semantics of Minker. The overall development has been influenced by the games studied for PCF and functional programming in general, in the styles of Abramsky–Jagadeesan–Malacaria and Hyland–Ong–Nickau.     

Imperative programs as proofs via game semantics

Game semantics extends the Curry–Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Laird?s sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language.     

Algebraic semantics and model completeness for Intuitionistic Public Announcement Logic

In the present paper, we start studying epistemic updates using the standard toolkit of duality theory. We focus on public announcements, which are the simplest epistemic actions, and hence on Public Announcement Logic (PAL) without the common knowledge operator. As is well known, the epistemic action of publicly announcing a given proposition is semantically represented as a transformation of the model encoding the current epistemic setup of the given agents; the given current model being replaced with its submodel relativized to the announced proposition. We dually characterize the associated submodel-injection map as a certain pseudo-quotient map between the complex algebras respectively associated with the given model and with its relativized submodel. As is well known, these complex algebras are complete atomic BAOs (Boolean algebras with operators). The dual characterization we provide naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). Thanks to this construction, the benefits and the wider scope of applications given by a point-free, intuitionistic theory of epistemic updates are made available. As an application of this dual characterization, we axiomatize the intuitionistic analogue of PAL, which we refer to as IPAL, prove soundness and completeness of IPAL w.r.t. both algebraic and relational models, and show that the well known Muddy Children Puzzle can be formalized in IPAL.     

Relating Categorical Semantics for Intuitionistic Linear Logic

There are several kinds of linear typed calculus in the literature, some with their associated notion of categorical model. Our aim in this paper is to systematise the relationship between three of these linear typed calculi and their models. We point out that mere soundness and completeness of a linear typed calculus with respect to a class of categorical models are not sufficient to identify the most appropriate class uniquely. We recommend instead to use the notion of internal language when relating a typed calculus to a class of models. After clarifying the internal languages of the categories of models in the literature we relate these models via reflections and coreflections. Mathematics Subject Classifications (2000) 03G30, 03B15, 18C50, 03B20.     

基于有限迁移系统的线性时态逻辑的计量化方法

基于有限迁移系统中全体无穷初始路径之集上的某种均匀概率测度,定义迁移系统TS对于LTL公式φ的满足度,并指出该概念是"TS满足φ"这一概念的计量化推广。在满足度理论的基础上,引入LTL公式之间的相似度,并诱导全体LTL公式之集上的伪距离,从而构建LTL逻辑度量空间。     

A Conditional Logic Approach for Strengthening Mixed 0-1 Linear Programs

We study a conditional logic approach for tightening the continuous relaxation of a mixed 0-1 linear program. The procedure first constructs quadratic inequalities by computing pairwise products of constraints, and then surrogates modified such inequalities to produce valid linear restrictions. Strength is achieved by adjusting the coefficients on the quadratic restrictions. The approach is a unifying framework for published coefficient adjustment methods, and generalizes the process of sequential lifting. We give illustrative examples and discuss various extensions, including the use of more complex conditional logic constructs that compute and surrogate polynomial expressions, and the application to general integer programs. Partially supported by NSF grant #DMI-0423415 and ONR grant #N00014-97-1-0784.     

A Decision Procedure for Nonperiodic Sequents of the First-Order Linear Temporal Logic

A deduction-based decision procedure is presented for the nonperiodic D-sequents of the first-order linear temporal logic. The D-sequents are obtained from D ₂-sequents [7], [8] by removing the periodicity condition. The deductive procedure proposed consists of decidable deductive procedures that replace infinitary and finitary induction rules for the temporal operator ``always'. The soundness and completeness of the deduction-based decision procedure proposed is proved.     

A parallel algorithm for partially separable non-convex global minimization: Linear constraints

The global minimization of large-scale partially separable non-convex problems over a bounded polyhedral set using a parallel branch and bound approach is considered. The objective function consists of a separable concave part, an unseparated convex part, and a strictly linear part, which are all coupled by the linear constraints. These large-scale problems are characterized by having the number of linear variables much greater than the number of nonlinear variables. An important special class of problems which can be reduced to this form are the synomial global minimization problems. Such problems often arise in engineering design, and previous computational methods for such problems have been limited to the convex posynomial case. In the current work, a convex underestimating function to the objective function is easily constructed and minimized over the feasible domain to get both upper and lower bounds on the global minimum function value. At each minor iteration of the algorithm, the feasible domain is divided into subregions and convex underestimating problems over each subregion are solved in parallel. Branch and bound techniques can then be used to eliminate parts of the feasible domain from consideration and improve the upper and lower bounds. It is shown that the algorithm guarantees that a solution is obtained to within any specified tolerance in a finite number of steps. Computational results obtained on the four processor Cray 2, both sequentially and in parallel on all four processors, are also presented.     

A majorizing semantics for hyperarithmetic sentences

A hyperarithmetic language is considered, obtained by adding to the arithmetic language a special ternary predicateH which acts as the universal predicate for (for some scale of constructive ordinals ). The language expresses a hierarchy {}_< of classes of formulas which is the constructive analog of the initial -section of the classical hyperarithmetic hierarchy. Some properties of this hierarchy are introduced which give a convenient constructive theoryT . It is shown that the majorizing semantics introduced in [1] (for an equivalent variant see [2]) can be extended to the sentences of the language for sentences of the arithmetic language. The basis for the construction of the majorant is the idea (stated in [2]) of relating the majorant to deducibility in systems with an -rule.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 68, pp. 30–37, 1977.     

The semantics and complexity of parallel programs for vector computations. Part I: A case study using ADA

Recent research in parallel numerical computation has tended to focus on the algorithmic level. Less attention has been given to the programming level where algorithm is matched, to some extent, to computer architecture. This two-part paper presents a three-level approach to parallel programming which distinguishes between mathematical algorithm, program and computer architecture. In part I, we motivate our approach by a case study using the Ada language. In part II, a mathematical concept of parallel algorithm is introduced in terms of partial orders. This serves as the basis of a theory of parallel computation which makes possible a precise semantics and a precise criterion of complexity of parallel programs. It also suggests some notation for specifying parallel numerical algorithms. To illustrate the ideas presented in part II, we concentrate here on parallel numerical computations which have vector spaces as their central data type and which are intended to be executed on a multi-processor system. The Ada language, with its task constructs, allows one to program computer algorithms to be executed on multi-processor systems, rather than on vector (pipelined) architectures. To provide a concrete example of the general problem of programming parallel numerical algorithms for multi-processor computers, we do a case study of how Ada can be used to program the solution of a system of linear equations on such computers. The case study includes an analysis of complexity which addresses the cost of data movement and process control/synchronization as well as the usual arithmetic complexity.Dedicated to Peter Naur on the occasion of his 60th birthdayThis research was partially supported by NSF Grants DCR-8406290 & CCR-8712192.     

A denotational semantics ofLC2

The aim of this paper is to extend the classical sequent calculusLC to the second order. This task is realized by a semantical approach mixing the correlation spaces semantics ofLC on the one hand, and the analogy with the interpretation of systemF in coherent spaces on the other hand. This relies on the introduction of a new semantical object:noetherian correlation spaces.From the semantics we deduce the syntax of the second order classical sequent calculusLC2.     

A project game for PERT networks

An important topic in PERT networks is how to allocate the total expedition (or delay) for situations in which the project is not executed as planned. In order to do that we define a TU project game that satisfies some desirable properties from the management project and game theory point of view.     

Metric semantics for concurrency

An overview is given of work we have done in recent years on the semantics of concurrency, concentrating on semantic models built on metric structures. Three contrasting themes are discussed, viz. (i) uniform or schematic versus nonuniform or interpreted languages; (ii) operational versus denotational semantics, and (iii) linear time versus branching time models. The operational models are based on Plotkin's transition systems. Language constructs which receive particular attention are recursion and merge, synchronization and global nondeterminacy, process creation, and communication with value passing. Various semantic equivalence results are established. Both in the definitions and in the derivation of these equivalences, essential use is made of Banach's theorem for contracting functions.Dedicated to Peter Naur on the occasion of his 60th birthday     

线性逻辑和态极逻辑引论(Ⅱ)

本文是《线性逻辑和态极逻辑引论》一文的第二部分。文章致力于证明网(第1节)和态极逻辑(第2,3,4和5节)证明网部分尽管局限于其积线性逻辑框架,但仍不失其重要性。线性逻辑和态极逻辑均为Girard所创建,近期所发展起来的态极逻辑旨在于进一步揭示计算和逻辑的基本交互作用的本质。我们希望本文能对这一新的理论带来一些计算机科学方面的启示。     

线性逻辑和态极逻辑引论(Ⅰ)

《线性逻辑和态极逻辑引论》一文概述了由Girard分别于1986和2001所创建的线性逻辑和态极逻辑.线性逻辑和态极逻辑汲取于计算机科学并反之应用于其中,从根本上对数理逻辑进行了彻底的审视.全文分为两部分.本文是文章的第一部分,致力于线性逻辑的联结词、证明规则、可判定性性质和模型.文章的第二部分将研究证明网并简要介绍态极逻辑.证明网是证明的图式表示,是线性逻辑的主要创新之一.     

A private contributions game for joint replenishment

We study a non-cooperative game for joint replenishment by n firms that operate under an EOQ-like setting. Each firm decides whether to replenish independently or to participate in joint replenishment, and how much to contribute to joint ordering costs in case of participation. Joint replenishment cycle time is set by an intermediary as the lowest cycle time that can be financed with the private contributions of participating firms. We characterize the behavior and outcomes under undominated Nash equilibria.     

Infinitary Calculus without Loop Rules for Restricted Sequents of the First-Order Linear Temporal Logic

A restricted first-order linear temporal logic with temporal operators next and always is considered. We prove that for this logic one can construct a sequential calculus without loop rules, i.e., the rules containing a duplication of the main formula in the premises of these rules. This paper continues the previous work of the author, where an infinitary calculus without loop rules on the logical level, but containing the traditional loop antecedent rule for the operator always, was constructed. In this paper, in order to remove this loop rule we introduce a nonlocal rule allowing us to eliminate loops in the process of the proof search. The soundness and >-completeness of the constructed calculus is proved.     

A parallel algorithm for generalized networks

This paper presents an application of parallel computing techniques to the solution of an important class of planning problems known as generalized networks. Three parallel primal simplex variants for solving generalized network problems are presented. Data structures used in a sequential generalized network code are briefly discussed and their extension to a parallel implementation of one of the primal simplex variants is given. Computational testing of the sequential and parallel codes, both written in Fortran, was done on the CRYSTAL multicomputer at the University of Wisconsin, and the computational results are presented. Maximum efficiency occurred for multiperiod generalized network problems where a speedup approximately linear in the number of processors was achieved.This research was supported in part by NSF grants DCR-8503148 and CCR-8709952 and by AFOSR grant AFOSR-86-0194.     

A framework for reasoning under uncertainty based on non-deterministic distance semantics

In this paper, we introduce a general and modular framework for formalizing reasoning with incomplete and inconsistent information. Our framework is composed of non-deterministic semantic structures and distance-based considerations. This combination leads to a variety of entailment relations that can be used for reasoning about non-deterministic phenomena and are inconsistency-tolerant. We investigate the basic properties of these entailments, as well as some of their computational aspects, and demonstrate their usefulness in the context of model-based diagnostic systems.