61.

Parametric Completeness for Separation Theories
- James Brotherston; Jules Villard
In this paper, we address the logical gap between provability in the logic BBI, which is the standard propositional basis for separation logic, and validity in an intended class of separation models, as employed in applications of separation logic such as program verification. An intended class of separation models is usually specified by a collection of axioms describing various useful model properties, which we call a separation theory. Our three main contributions are as follows. First, we show that that several important properties of separation models are not definable in BBI. Second, we show that these properties become definable when...

62.

Non-deterministic Phase Semantics and the Undecidability of Boolean BI
- Dominique Larchey-Wendling; Didier Galmiche
We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered as the “core” of Separation and Spatial Logics. For this, we define a complete phase semantics suitable for BBI and characterize it as trivial phase semantics. We deduce an embedding between trivial phase semantics for intuitionistic linear logic (ILL) and Kripke semantics for BBI. We single out the elementary fragment of ILL which is both undecidable and complete for trivial phase semantics. Thus, we obtain the undecidability of BBI.

63.

From Hyperedge Replacement to Separation Logic and Back
- Mike Dodds; Detlef Plump
Hyperedge-replacement grammars and separation-logic formulas both define classes of graph-like structures. In this paper, we relate the different formalisms by effectively translating restricted hyperedge-replacement grammars into formulas of a fragment of separation-logic with recursive predicates, and vice versa. The translations preserve the classes of specified graphs, and hence the two approaches are of equivalent power. It follows that our fragment of separation-logic inherits properties of hyperedge-replacement grammars, such as inexpressibility results. We also show that several operators of full separation logic cannot be expressed using hyperedge replacement.

64.

A cut-free proof theory for Boolean BI (via display logic)
- James Brotherston
We give a display calculus proof system for Boolean BI (BBI) based on Belnap’s general display logic. We show that cut-elimination holds in our system and that it is sound and complete with respect to the usual notion of validity for BBI. We then show how to constrain proof search in the system (without loss of generality) by means of a series of proof transformations. By doing so, we gain some insight into the problem of decidability for BBI.

65.

From Hyperedge Replacement to Separation Logic and Back
- Mike Dodds; Detlef Plump
Hyperedge-replacement grammars and separation-logic formulas both define classes of graph-like structures. In this paper, we relate the different formalisms by effectively translating restricted hyperedge-replacement grammars into formulas of a fragment of separation-logic with recursive predicates, and vice versa. The translations preserve the classes of specified graphs, and hence the two approaches are of equivalent power. It follows that our fragment of separation-logic inherits properties of hyperedge-replacement grammars, such as inexpressibility results. We also show that several operators of full separation logic cannot be expressed using hyperedge replacement.

66.

Formalizing Trust-based Decision Making in Electronic Commerce Transactions
- Tyrone Grandison; Han Reichgelt
Trust is the cornerstone of traditional business transactions and a lack of trust is one of the main inhibitors on the future growth of Electronic Commerce. However, trust is a nebulous social construct that is further complicated by its context dependence. Our assertion is that through study of the contextual artifacts and the process of trust formation in traditional business settings, we can devise a logic-based model that adequately captures the constructs needed to enable the automated creation of trusted Electronic Commerce transactions. In this paper, we introduce a model, called E2T2, which enables the creation of trust-based relationships between...

67.

Erdős Graphs Resolve Fine's Canonicity Problem
- Robert Goldblatt; Ian Hodkinson; Yde Venema
We show that there exist 2^ℵ0 equational classes of Boolean algebras with operators that are not generated by the complex algebras of any first-order definable class of relational structures. Using a variant of this construction, we resolve a long-standing question of Fine, by exhibiting a bimodal logic that is valid in its canonical frames, but is not sound and complete for any first-order definable class of Kripke frames. The constructions use the result of Erdős that there are finite graphs with arbitrarily large chromatic number and girth.

68.

THE ANALOGUE OF BÜCHI’S PROBLEM FOR RATIONAL FUNCTIONS
- Thanases Pheidas; Xavier Vidaux
Büchi’s problem asked whether there exists an integer M such that the surface defined by a system of equations of the form x 2 n + x2n−2 =2x2n−1 +2, n =2,...,M − 1, has no integer points other than those that satisfy ±xn = ±x0 + n (the ± signs are independent). If answered positively, it would imply that there is no algorithm which decides, given an arbitrary system Q =(q1,...,qr) of integral quadratic forms and an arbitrary r-tuple B =(b1,...,br) of integers, whether Q represents B (see T. Pheidas and X. Vidaux, Fund. Math. 185 (2005) 171–194). Thus it...

69.

Arquitetura computacional alternativa implementada com lógica Fuzzy
- Klein, Pedro A.T.; Figueredo, Melissa G.; Weber, Leo
70.

Decifrando a caixa preta do cinema de animação : arqueologia dos modos de produção de imagens técnicas
- Schneider, Carla
Esta tese investiga transformações nos modos de produção das imagens do cinema de animação, na perspectiva do pós ao pré-cinema. O problema da pesquisa advém de experiências práticas observadas e vivenciadas e encontra embasamento em estudos sobre as especificidades técnicas e culturais ― percebidas na produção de tais imagens ― à luz de conceitos desenvolvidos por Vilém Flusser (caixa preta, aparelho, imagens técnicas), Lev Manovich (animação como lógica processual do cinema), Lucia Santaella (paradigmas evolutivos da imagem) e Richard Sennett (o dilema entre o artífice-artesão e as máquinas). Com o propósito de compreender tais transformações, o presente trabalho é norteado...

71.

Gröbner Bases Computation in Strand: A Case Study for Concurrent Symbolic Computation in Logic Programming Languages
- Kurt Siegl
This thesis studies the adequacy of parallel logic programming languages for the purpose of parallel symbolic computation. We conclude that the languages of the guarded Horn clause type are best suited for parallel Symbolic Computation. Various programming examples show that the usage of logic languages is a major step forward in parallel programming. In a case study we describe a novel approach to the parallelization of Buchberger's Gröbner bases algorithm using a medium grain pipe-line principle for the polynomial reduction. The approach is implemented in STRAND88 on a 17 transputer distributed memory system and shows a remarkable speed-up.

72.

Constraint Logic Programming -- An Informal Introduction
- Thom Frühwirth; Alexander Herold; Volker Küchenhoff; Thierry Le Provost; Pierre Lim; Eric Monfroy, Mark Wallace
Constraint Logic Programming (CLP) is a new class of programming languages combining the declarativity of logic programming with the efficiency of constraint solving. New application areas, amongst them many different classes of combinatorial search problems such as scheduling, planning or resource allocation can now be solved, which were intractable for logic programming so far. The most important advantage that these languages offer is the short development time while exhibiting an efficiency comparable to imperative languages. This tutorial aims at presenting the principles and concepts underlying these languages and explaining them by examples. The objective of this paper is not to...

73.

Mafia behaviour and the evolution of facultative virulence
- Juan Jose Soler; Anders Pape Møller; Manuel Soler
Some organisms enforce "maladaptive" behaviours on others of the same or different species by imposing costs in the absence of compliance. Such enforcement is used by the enforcer to obtain benefits in the possession of the enforced individual. This mechanism is known as mafia behaviour in humans, but may be widespread in parasite–host relationships in nature, from the cellular level to societies. In this paper we describe the evolution of such mafia mechanisms, and we propose a fuzzy logic model where the mafia mechanism is based on enforcement of hosts by exponentially increasing the cost of resistance to the parasite....

74.

A Parallel Prolog Resolution Based on Multiple Unifications
- I. Vlahavas; P. Kefalas
This paper presents two algorithms as extensions to the basic Resolution Principle of logic programs which exploit parallelism retaining the full semantics of Prolog. The first algorithm, called SPU, allows parallel execution of unifications belonging to deterministic paths of the proof tree, giving in effect AND-parallel execution. The second algorithm, called MPU, retains the benefits of SPU while exploiting OR-parallelism. We also present simulation results which are indicative of the performance of the proposed algorithms and finally we discuss implementation issues which give rise to the development of a parallel machine.

75.

Generating Functions For Kernels of Digraphs (Enumeration & Asymptotics for Nim Games)
- Cyril Banderier; Jean-marie Le Bars; Vlady Ravelomanana
In this article, we study directed graphs (digraphs) with a coloring constraint due to Von Neumann and related to Nim-type games. This is equivalent to the notion of kernels of digraphs, which appears in numerous fields of research such as game theory, complexity theory, artificial intelligence (default logic, argumentation in multi-agent systems), 0-1 laws in monadic second order logic, combinatorics (perfect graphs)... Kernels of digraphs lead to numerous difficult questions (in the sense of NP-completeness, #P-completeness). However, we show here that it is possible to use a generating function approach to get new informations: we use technique of symbolic and...

76.

Accelerated Adaptive Markov Chain for Partition Function Computation
- Stefano Ermon; Carla P. Gomes; Ashish Sabharwal; Bart Selman
We propose a novel Adaptive Markov Chain Monte Carlo algorithm to compute the partition function. In particular, we show how to accelerate a flat histogram sampling technique by significantly reducing the number of “null moves ” in the chain, while maintaining asymptotic convergence properties. Our experiments show that our method converges quickly to highly accurate solutions on a range of benchmark instances, outperforming other state-of-the-art methods such as IJGP, TRW, and Gibbs sampling both in run-time and accuracy. We also show how obtaining a so-called density of states distribution allows for efficient weight learning in Markov Logic theories.

77.

UTILIZING MOMENT INVARIANTS AND GRÖBNER BASES TO REASON ABOUT SHAPES
- Haim Schweitzer; Janell Straach
Shapes such as triangles or rectangles can be defined in terms of geometric properties invariant under a group of transformations. Complex shapes can be described by logic formulae with simpler shapes as the atoms. A standard technique for computing invariant properties of simple shapes is the method of moment invariants, known since the early sixties. We generalize this technique to shapes described by arbitrary monotone formulae (formulae in propositional logic without negation). Our technique produces a reduced Gröbner basis for approximate shape descriptions. We show how to use this representation to solve decision problems related to shapes. Examples include determining...

78.

Definição de qualidade no serviço público municipal da cidade de Porto
Alegre; indicadores e lógica subjacente.
- Coelho, Diego Traesel
79.

Simulação lógica visual 3D de circuitos integrados usando modelos VRML.
- Ost, Luciano C.
80.

Um ambiente interativo para o desenvolvimento de provas da lógica proposicional.
- Alves, Gleifer V.; Dimuro, Graçaliz Pereira; Costa, Antônio Carlos da Rocha