Search

This paper develops an inference system for natural language within the ‘Natural Logic’ paradigm as advocated by van Benthem (1997), Sánchez (1991) and others. The system that we propose is based on the Lambek calculus and works directly on the Curry-Howard counterparts for syntactic representations of natural language, with no intermediate translation to logical formulae. The Lambek-based system we propose extends the system by Fyodorov et~al. (2003), which is based on the Ajdukiewicz/Bar-Hillel (AB) calculus Bar Hillel, (1964). This enables the system to deal with new kinds of inferences, involving relative clauses, non-constituent coordination, and meaning postulates that involve complex expressions. Basing the system on the Lambek calculus leads to problems with non-normalized proof terms, which are treated by using normalization axioms.This paper develops an inference system for natural language within the ‘Natural Logic’ paradigm as advocated by van Benthem (1997), Sánchez (1991) and others. The system that we propose is based on the Lambek calculus and works directly on the Curry-Howard counterparts for syntactic representations of natural language, with no intermediate translation to logical formulae. The Lambek-based system we propose extends the system by Fyodorov et~al. (2003), which is based on the Ajdukiewicz/Bar-Hillel (AB) calculus Bar Hillel, (1964). This enables the system to deal with new kinds of inferences, involving relative clauses, non-constituent coordination, and meaning postulates that involve complex expressions. Basing the system on the Lambek calculus leads to problems with non-normalized proof terms, which are treated by using normalization axioms.

Abstract Unification grammars are known to be Turing-equivalent; given a grammar G and a word w, it is undecidable whether w ? L(G). In order to ensure decidability, several constraints on grammars, commonly known as off-line parsability (OLP), were suggested, such that the recognition problem is decidable for grammars which satisfy OLP. An open question is whether it is decidable if a given grammar satisfies OLP. In this paper we investigate various definitions of OLP and discuss their interrelations, proving that some of the OLP variants are indeed undecidable. We then present a novel, decidable OLP constraint which is more liberal than the existing decidable ones.

We suggest a new semantic interpretation of interrogative NPs, based on a novel algebraic theory of the semantics of questions. We discuss the role of interrogative NPs in compositionally deriving the semantics of wh-questions, examine the coordination of interrogative NPs, and apply notions from generalized quantifier theory to their interpretation.

Typed feature structures are used extensively for the specification of linguistic information in many formalisms. The subsumption relation orders TFSs by their information content. We prove that subsumption of acyclic TFSs is well founded, whereas in the presence of cycles general TFS subsumption is not well founded. We show an application of this result for parsing, where the well-foundedness of subsumption is used to guarantee termination for grammars that are off-line parsable. We define a new version of off-line parsability that is less strict than the existing one; thus termination is guaranteed for parsing with a larger set of grammars.

The paper identifies a problem in default reasoning in Reiter’s Default Logic and related systems: elements which are similargiven the axioms only, become distinguishable in extensions. We explain why, sometimes, this is considered undesirable. Two approaches are presented for guaranteeing similarity preservation: One approach formalizes a way of uniformly applying the defaults to all similar elements by introducing generic extensions, which depend only on similarity types of objects. According to the second approach, for a restricted class of default theories, a default theory is viewed as a “shorthand notation” to what is “really meant” by its formulation. In this approach we propose a rewritingof defaults in a form that guarantees similarity preservation of the modified theory. It turns out that the above two approaches yield the same result.

In this paper, a new fairness notion is proposed for languages withmulti-party interactions as the sole interprocess synchronization and communication primitive. The main advantage of this fairness notion is the elimination of starvation occurring solely due to race conditions (i.e., ordering of independent actions). Also, this is the first fairness notion for such languages which is fully adequate with respect to the criteria presented in [2]. The paper defines the notion, proves its properties, and presents examples of its usefulness.

The relations among various languages and models for distributed computation and various possible definitions of fairness are considered. Natural semantic criteria are presented which an acceptable notion of fairness should satisfy. These are then used to demonstrate differences among the basic models, the added power of the fairness notion, and the sensitivity of the fairness notion to irrelevant semantic interleavings of independent operations. These results are used to show that from the considerable variety of commonly used possibilities, only strong process fairness is appropriate forCSP if these criteria are adopted. We also show that under these criteria, none of the commonly used notions of fairness are fully aceptable for a model with an n-way synchronization mechanism. The notion of fairness most often mentioned for Ada is shown to be fully acceptable. For a model with nonblockingsend operations, some variants of common fairness definitions are appraised, and two are shown to satisfy the suggested criteria.

The paper considers the treatment of fairness assumptions which arenot equivalence-robust, a central issue in relatinginterleaving semantics topartial order semantics. A notion ofcompletion is introduced and studied, and two specific completions are considered:maximal completion, which is easier to implement (shown by a broadcast bus implementation) but guarantees only weak liveness properties of programs using it; andminimal completion, which may be harder to implement but induces stronger liveness properties on programs using it. Some properties of completions are formulated. Finally, the impact of non-equivalence-robustness on compositionality with respect to separate fairness assumptions is considered.

We consider the specification and verification of cyclic (sequential and concurrent) programs. The input-output based concept of correctness traditionally applied to functional programs is replaced by another, based on the concept of eventual behaviour. Various types of eventual behaviour are introduced. In the case of concurrency, the introduction of interface-predicates reduces the proof complexity and achieves greater readability. All specifications use explicitly the auxiliary variables of a location counter p and elapsing time t.

Program composition and compositional proof systems have proved thermselves important for simplifying the design and the verification of programs. The paper presents a version of the jigsawprogram composition operator previously defined in [Fix et al. (1991, 1992)]. Here, the jigsaw operator is defined as the unification of its components by their most general unifier. The jigsaw operator generalizes and unifies the traditional sequentialand parallelprogram composition operators and the newly proposed unionand superpositionoperators. We consider a family of frameworks each consisting of a programming language, a specification language and a compositional syntax-directed proof system. We present syntactic rules to augment any given framework in the family with the jigsaw operator. The augmented framework is syntax-directed and compositional. Moreover, it is sound and complete with respect to the given framework.

In this paper, we view computer networks as distributed systems that provide their users with a set of services, in a way which hides the distinction between those services which are local and those which are remote. We conceive of a given target network configuration as a network of communicating virtual machines and its behavior is modelled by a system of communicating sequential processes. Network protocols are described by a high level concurrent language (CSP) and a methodology is developed which permits the verification of partial and total correctness assertions about the system in a simple and natural way. Global invariants are used to establish invariant properties of the whole system and histories to record the sequence of communication exchanges between every matching pair of processes. Eventuality properties are expressed using linear temporal logic.

Many recent axiomatic definitions for structured programming languages include control predicates,at(S), in(S), andafter(S), which are an abstraction of location counters. The usual axioms identify control locations so as to imply that “no time” (i.e., no state transition) is needed to pass from the end of one statement to the next, and in particular from the end of a loop body back to the test at the head of the loop. Here, an axiomatic framework for control predicates is examined. It is shown that if all the axioms are to be maintained with common representation mappings, there are difficult new requirements which need to be satisfied by an implementation for fair concurrent models of computation. Several approaches to resolving the difficulty are considered, and in particular it is suggested to replace some axioms of the formP?Q byP?eventually(Q), whereP andQ are control predicates, thereby separating control states previously identified.

The paper presents a family of properties of programs, called product (and power) properties, for which the verification method of Floyd and Hoare are inconvenient. A (semantically) complete alternative method is proposed' The paper presents the method in both the endogenous and exogenous versions and applies them to examples. Semantic completeness and soundness are shown. The method is particularly useful for some second-order programs, having procedures as parameters.

A mathematical (denotational) semantics is constructed for a formalism of recursive equations with the Alternative operator. This formalism enables the combination of recursion and backtracking. The semantics is defined by applying fixpoint theory to set valued functions. We introduce the notion of strategy to produce subsets of the result. Two implementations are suggested using an auxiliary stack, that trade off recomputation time with space in the auxiliary stack. The concept of a sub-fixpoint is introduced, and the implementations are shown to be incomplete even w.r.t. sub-fixpoint values. One special strategy, the leftmost strategy, which stems from problems such as pattern matching or parsing, is discussed.

Focuses on the positional and keyword parameter communication with subprograms in structured programming. Comparison between keyword notation and positional notation; Discussion about various categories of notation; Efficacy of the transmission of the models.

In this paper I introduce the notion of bilogics, namely logics interpreted over a pair of structures, in contrast to classical logic and many of its variations, the formulae of which are interpreted over one structure. In particular, I introduce and study Contrastive Logic, suitable for expressing contrast and conformity between the two structures involved. A major reason for this study is striving towards an extension of truth-conditional semantics to cover several natural-language particles, which have been hitherto considered not to be amenable to such an extensional treatment, and were delegated to the level of non-extensional pragmatics. Examples of such particles are but and already.