401.
Properties of the Lattice of Observables in Logic Programming
- Gianluca Amato; Giorgio Levi
We show several properties of the abstract interpretation settings regarding relationships between precision of semantic operators and abstract domains composition. Then, we apply these results to the framework for logic programs introduced in [3], extended with the new class of operational observables. We prove that the classes of perfect, denotational and operational observables are complete lattices and we discuss some problems that arise studying them. Finally, we show how to use functional dependencies to systematically derive new domains in which our semantic operators enjoy desired precision properties. keywords: logic programming, semantics, compositionality, abstract interpretation, abstract semantics. 1 Introduction Our goal...
402.
Default Quantifier Logic
. In this paper we present a powerful uniform
first-order framework for representing and reasoning with
complex forms of default knowledge. This is achieved by
extending first-order predicate logic with a new generalized
quantifier, anchored in the quasi-probabilistic ranking
measure paradigm [Weydert 94], which subsumes and
refines the original, propositional notion of a default conditional
[Delgrande 88, Weydert 91, Boutilier 94].
1. INTRODUCTION
In recent times, default conditionals interpreted by ranking
measures or order-of-magnitude probability distributions
have become an increasingly popular tool for encoding
defeasible relationships. Conceptual adequacy, semantic
transparency, probabilistic justifications, the existence
of proof-theoretic characterizations, the correct,
natural handling of specificity and the availability of promising
nonmonotonic inference relations [Weydert 96]
are strong arguments in...
403.
Parallel Logic Programming Techniques
Model [War87a] x x
16 Delphi [CA88] x x
17 Randomize Method [JAM88] x x
18 ORBIT [YN84] ? ? ?
19 VMHW model [VXDRS91] ? ? ?
20 VMBA model [VXDRS91] ? ? ?
Table 2.1: Time complexity of operations in OR-parallel methods [Gup94]. A cross indicates
constant time operation, a blank usually means linear time operation.
IMPACT-NLI-1998-3
12 2 Parallel Logic Programming IMPACT
by proper selection of algorithms. For example, instead of computing the factorial
by multiplying consecutive increasing numbers, it is also possible to use a divide and
conquer technique. The latter will allow independent AND-parallelism, whereas the
former will not allow any form of AND-parallelism.
2.3.1 Implementing Independent AND-Parallelism
In order...
404.
Constraint (Logic) Programming: A Bibliography
ion for unstructured
CSPs. In SARA'92: Proceedings of the Symposium on Abstraction, Reformulation, and
Approximation, pages 126--133, 1992. http://www.cs.utexas.edu/users/schrag/SARA.ps.
[733] R. Schrag and D. Miranker. Abstraction and the CSP phase transition boundary. In
SAIM'95: Proceedings of the 4th International Symposium on Artificial Intelligence and
Mathematics, pages 126--133, 1995. http://www.cs.utexas.edu/users/schrag.
[734] D. De Schreye and M. Bruynooghe. The compilation of forward checking regimes through
meta-interpretation and transformation. In H. Abramson and M. H. Rogers, editors, MetaProgramming
in Logic Programming, pages 217--232. MIT Press, 1989.
[735] A. Schrijver. Theory of Linear and Integer Programming. Wiley and Sons, 1986.
[736] Christian Schulte, Gert Smolka, and Jorg Wurtz. Encapsulated search and constraint programming
in Oz....
405.
The Design Logic Project
ve
three research programs available as part of the project by
the end of 1997. The overall arrangement of the project
will initially follow the Artifact-Centered Modeling framework
I have developed [Sal95]. Within the framework,
the two main points of interest will be (a) development
of formal (logical) theories, and (b) implementations of
computer-based tools.
The first research program is developing a formal theory
of product information, called the Axiomatic Information
Model for Design (AIM-D). AIM-D interprets axiomatic
set theory to provide a rigorous system for product description.
The theory covers assemblies, parts, features,
and quantities, and an axiomatization of type information
about products. Besides showing that there exist equivalences
between well-understood systems of logic...
406.
Games in Philosophical Logic
Semantic games are an important evaluation method for a
wide range of logical languages, and are frequently resorted to
when traditional methods do not easily apply. A case in point
is a family of independence-friendly (IF) logics which allow regulation
over information flow in formulas, and thus perfect information
fails in the games associated with such formulas. This
mechanism of imperfect information is studied in this paper. It
is noted that imperfect information of players often gives rise
to the game-theoretic phenomenon of imperfect recall. Furthermore,
independence-friendliness in epistemic logic is investigated.
We also discuss a couple of misunderstandings that have occurred
in the literature concerning IF first-order logics and gametheoretical
semantics,...
407.
ADAPTIVE FUZZY LOGIC CONTROLLER
- Willy K. Wojsznis; Dirk Thiele; John Gudaz
This paper describes background and design of a model free adaptive Fuzzy Logic Controller. Controller Error Scaling Factor adaptation uses principle of balancing Error and Change of Error actions. Adaptation proceeds only if prescribed set of conditions is satisfied. Controller Scaling Factor for Change of Output adaptation uses weighted average of correction from oscillation index and process steady state gain estimates. Interaction between Scaling Factor of Output adaptation and Scaling Factor of Error adaptation has been alleviated by applying different adaptation speed for the two parameters and by using corrective calculations. The distinctive feature of the tuner design is simplicity....
408.
Tableau Reasoning and Programming with Dynamic First Order Logic
- Jan van Eijck; Juan Heguiabehere; Breanndan O Nuallain
Dynamic First Order Logic (DFOL) results from interpreting quantification over a variable v as change of valuation over the v position, conjunction as sequential composition, disjunction as nondeterministic choice, and negation as (negated) test for continuation. We present a tableau style calculus for DFOL with explicit (simultaneous) binding, prove its soundness and completeness, and point out its relevance for programming with DFOL, for automated program analysis including loop invariant detection, and for semantics of natural language. Next, we extend this to an infinitary calculus for DFOL with iteration and connect up with other work in dynamic logic.
409.
The Inverse Method for Intuitionistic Linear Logic (The Propositional Fragment)
- Kaustuv Chaudhuri
We present a forward sequent calculus for intuitionistic propositional linear logic (# , 1, 0, !) and a corresponding inverse-method search strategy. Our approach centres around resource management, inspired by similar approaches for backward-directed calculi such as top-down linear logic programming. Surprisingly, the resource management problems for the forward direction turn out to have a different character to those of the backward direction, arising for different connectives. Our approach identifies conditions for which we may relax linearity to allowing (implicit) weakening. We characterize two such classes of affine behaviour -- as a form of weak sequent designed to handle #-weakening...
410.
Clocking Structures and Power Analysis for Nanomagnet-Based Logic Devices
- M. T. Niemier; X. S. Hu
Logical devices made from nano-scale magnets have many potential advantages – systems should be non-volatile, dense, low power, radiation hard, and could have a natural interface to MRAM. Initial work includes experimental demonstrations of logic gates and wires and theoretical studies that consider their power dissipation. This paper looks at power dissipation too, but also considers the circuitry needed to drive a computation. Initial results are very encouraging and indicate that clocked magnetic logic could – in the worst case – match equivalent low power CMOS circuits and – in the bestcase – potentially provide more than 2 orders of...
411.
IOS Press Strong Normalisation of Cut-Elimination in Classical Logic
- C. Urban; Marseille France; G. M. Bierman
Abstract. In this paper we present a strongly normalising cut-elimination procedure for classical logic. This procedure adapts Gentzen’s standard cut-reductions, but is less restrictive than previous strongly normalising cut-elimination procedures. In comparison, for example, with works by Dragalin and Danos et al., our procedure requires no special annotations on formulae and allows cut-rules to pass over other cut-rules. In order to adapt the notion of symmetric reducibility candidates for proving the strong normalisation property, we introduce a novel term assignment for sequent proofs of classical logic and formalise cut-reductions as term rewriting rules.
412.
The Inverse Method for Intuitionistic Linear Logic (The Propositional Fragment)
- Kaustuv Chaudhuri
We present a forward sequent calculus for intuitionistic propositional linear logic (# , 1, N, , 0, !) and a corresponding inverse-method search strategy. Our approach centres around resource management, inspired by similar approaches for backward-directed calculi such as top-down linear logic programming. Surprisingly, the resource management problems for the forward direction turn out to have a different character to those of the backward direction, arising for different connectives. Our approach identifies conditions for which we may relax linearity to allowing (implicit) weakening. We characterize two such classes of affine behaviour -- as a form of weak sequent designed to...
413.
Temporal Logic
- Yde Venema; Lou Goble (ed; Blackwell Guide; Philosophical Logic; Blackwell Publishers
this paper, section 3, is devoted to a fairly detailed exposition of Prior's basic tense logic; the aim of this is not only to introduce the readers to this particular system, but perhaps even more to acquaint them with the kind of questions that temporal logicians tend to ask. In the sections 4 and 5 we present some extensions and alternatives to this base system. In section 6 we sketch some developments that have taken place over the last ten years or so. Finally, in the epilogue we try to answer the question what Temporal Logic is; this section also...
414.
APLICAÇÃO DOS MÉTODOS DA LÓGICA DIFUSA NADEFINIÇÃO DE SISTEMAS ESTRUTURAIS DE EDIFÍCIOS
- Paulo André Rabelo Alkmin
Atualmente, em meio à grande variedade de processos e sistemas construtivosdisponíveis no mercado, o profissional da construção civil freqüentemente se deparacom várias questões do tipo: Qual sistema estrutural é o mais eficiente para o meuempreendimento? Deve ser em aço ou em concreto? Deve ser industrializado ouartesanal, ou deve ser ainda uma combinação de mais de um sistema?Essas escolhas são de fundamental importância para a eficiência da obra e para osucesso do empreendimento. É importante salientar que tais definições devem ser feitasantes mesmo do projeto arquitetônico, visto que um bom projeto de arquitetura deve tersua concepção baseada nos princípios e peculiaridades...
415.
Propositional Logic of Imperfect Information: Foundations and Applications
- Pietarinen, Ahti-Veikko
I will show that the semantic structure of a new imperfect-information propositional logic can be described in terms of extensive forms of semantic games. I will discuss some ensuing properties of these games such as imperfect recall, informational consistency, and team playing. Finally, I will suggest a couple of applications that arise in physics, and most notably in quantum theory and quantum logics.
416.
Semantics of Well-Moded Input-Consuming Logic Programs
- Annalisa Bossi; Sandro Etalle; Sabina Rossi
Recent logic programming languages employ dynamic scheduling of calls to improve efficiency of programs. Dynamic scheduling is realized by allowing some calls to be dynamically "delayed" until their arguments are sufficiently instantiated. To this end, logic languages are extended with constructs such as delay declarations. However, many declarative properties that hold for logic and pure Prolog programs do not apply any longer in this extended setting. In particular, the equivalence between the model-theoretic and operational semantics does not hold. In this paper, we study the class of input-consuming programs. Firstly, we argue that input-consuming logic programs are suitable for modeling...
417.
2 CLL: A Traditional Sequent Calculus for Linear Logic 1
- Frank Pfenning
We present a new proof of cut elimination for linear logic which proceeds by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. The computational content of this proof is a non-deterministic algorithm for cut elimination which is amenable to an elegant implementation in Elf. We show this implementation in detail.
418.
Lossless binary image compression using logic functions and spectra
- Bogdan J. Falkowski
A lossless compression of images using coding schemes and patterns that include minterm, cube and coordinate data coding, Walsh, triangular and Reed–Muller weights based patterns, Reed–Muller spectra and reference row technique is proposed. The experimental results indicate that the technique is fairly efficient when compared with other methods based on representations of logic functions.
419.
Temporal Disjunctive Logic Programming 1 Temporal Disjunctive Logic Programming
- Manolis Gergatsoulis; Panos Rondogiannis; Themis Panayiotopoulos; M. Gergatsoulis; P. Rondogiannis; T. Panayiotopoulos
Abstract In this paper we introduce the logic programming language Disjunctive Chronolog which combines the programming paradigms of temporal and disjunctive logic programming. Disjunctive Chronolog is capable of expressing dynamic behaviour as well as uncertainty, two notions that are very common in a variety of real systems. We present the minimal temporal model semantics and the xpoint semantics for the new programming language and demonstrate their equivalence. We also show how proof procedures developed for disjunctive logic programs can be easily extended to apply to Disjunctive Chronolog programs.
420.
Australasian Journal of Logic
