581.
Completeness proof of functional logic, a formalism with
variable-binding nonlogical symbols
- Schoenbrunner, Josef
We know extensions of first order logic by quantifiers of the kind "there are
uncountable many ...", "most ..." with new axioms and appropriate semantics.
Related are operations such as "set of x, such that ...", Hilbert's
$\epsilon$-operator, Churche's $\lambda$-notation, minimization and similar
ones, which also bind a variable within some expression, the meaning of which
is however partly defined by a translation into the language of first order
logic. In this paper a generalization is presented that comprises arbitrary
variable-binding symbols as non-logical operations. The axiomatic extension is
determined by new equality-axioms; models assign functionals to
variable-binding symbols. The completeness of this system of the so called
"Functional Logic...
582.
Challenge problems for the integration of logic and connectionist systems (Extended Abstract)
- Steffen Hölldobler
) Steen Holldobler Articial Intelligence Institute Department of Computer Science Dresden University of Technology D{01062 Dresden Phone: +49-351-463-8340 Fax: +49-351-463-8342 sh@inf.tu-dresden.de Keywords: Logic Programming, Recurrent Connectionist Networks 1 1 Motivation Connectionist systems exhibit many desirable properties of intelligent systems like, for example, being massively parallel, context{sensitive, adaptable and robust (see eg. [7]). It is strongly believed that intelligent systems must also be able to represent and reason about structured objects and structure{sensitive processes (see eg. [8, 23]). Unfortunately, we are unaware of any connectionist system which can handle structured objects and structure{sensitive processes in a satisfying way. Logic systems were...
583.
Performance Evaluation of Or-Parallel Logic Programming Systems on Distributed Shared-Memory Architectures
- Vanusa Menditi Calegario; Ines De Castro Dutra
. Distributed shared-memory (DSM) architectures have been object of research by many computer science groups. In this work, we investigate how DSM architectures affect performance of or-parallel logic programming systems and how this performance approaches that of conventional C systems. Our work concentrates on basic performance, scalability, and programmability. Keywords: logic programming, conventional programming, parallelism, DSM architectures, performance evaluation 1 Introduction Distributed shared-memory architectures have been object of research by many computer science groups. Research goes broadly from hardware based coherence protocols to DSM software protocols on networks of workstations passing through high technology inter-connection networks that reduce network latency....
584.
VisAll: A Universal Tool to Visualise the Parallel Execution of Logic Programs
- Nuno Fonseca; Vítor Santos Costa; V'itor Santos Costa; Inês de Castro Dutra
One of the most important advantages of logic programming systems is that they allow the transparent exploitation of parallelism. The different forms of parallelism available and the complex nature of logic programming applications present interesting problems to both the users and the developers of these systems. Graphical visualisation tools can give a particularly important contribution, as they are easier to understand than text based tools, and allow both for a general overview of an execution and for focusing on its important details. Towards these goals, we propose VisAll, a new tool to visualise the parallel execution of logic programs. VisAll...
585.
VisAll: A new Tool to Visualise the Parallel Execution of Logic Programs
- V'itor Santos Costa; Vítor Santos Costa; Ines de Castro Dutra; Ines De Castro; Nuno Fonseca; Nuno Fonseca; Costa Ines; Castro Dutra
One of the most important advantages of logic programming systems is that they allow the transparent exploitation of parallelism. The different forms of parallelism available and the complex nature of logic programming applications present interesting problems to both the users and the developers of these systems. Graphical visualisation tools can give a particularly important contribution, as they are easier to understand than text based tools, and allow both for a general overview of an execution and for focusing on its important details. Towards these goals, we propose VisAll, a new tool to visualise the parallel execution of logic programs. VisAll...
586.
A semantics for logic programs based on first order hereditary Harrop formulas
- Ernesto Lastres
The paper introduces a semantics for logic programs based on first order hereditary Harrop formulas which are expressed in terms of intuitionistic derivations. The derivations are constructed by means of an intuitionistic proof procedure that constitutes the resolution mechanism of the language. The semantics of a program is a goal independent denotation which can be equivalently specified by a denotational and an operational semantics. The denotational semantics is defined using a set of primitive semantic operators that act on derivations and are directly related to the properties of the derivations. Keywords: Logic Programming, Abstract Interpretation, Harrop Formulas 1 Introduction The...
587.
Goal Independency and Call Patterns in the Analysis of Logic Programs
- Maurizio Gabbrielli; Roberto Giacobazzi; Ecole Polytechnique
We propose an abstract semantics for the goal independent analysis of properties of "procedure calls" in SLD derivations (call patterns). This can be used to derive information useful for logic program optimizations. Keywords: Logic programs, abstract interpretation, procedure calls. 1 Introduction In this paper we consider a new application in the area of abstract interpretation based on the s-semantics approach [12, 3]. Several abstract interpretation frameworks based on this approach have been defined [15], including those based [2, 6] on the original s-semantics (modeling computed answer substitutions) [11]. Starting from the simplified version of an existing concrete semantics [14], here...
588.
Possibilistic Logic: Complexity and Algorithms
Possibilistic logic is a logic for reasoning with uncertain and partially inconsistent
knowledge bases. Its standard version consists in ranking propositional formulas according
to their certainty or priority level, by assigning them lower bounds of necessity values. We
give a survey of automated deduction techniques for standard possibilistic logic, together
with complexity results. We focus on the extensions of resolution (Section 3) and of the
Davis and Putnam procedure (Section 4). In Section 5 we consider extended versions
and variants of possibilistic logic. We conclude by listing the related research topics, the
applicative impact of this work and further research issues.
1 Introduction
Possibilistic logic is a logic of...
589.
A Negative Result for Chain Logic
We show that chain, path, nite chain and rst-order order logic (interpreted
over innite binary trees) cannot be nite automata characterized by
means of imposing restrictions on kinds of acceptance conditions of automata.
1 Introduction
Branching time temporal logic CTL
over binary trees is expressively equivalent to
the monadic second-order theory of two successors with set quantication restricted
to innite paths [HT 87]. In [Th 87] some other restricted versions of the monadic
second-order theory are considered: set quantication is allowed over chains and
nite chains, respectively. These subtheories can be seen as candidates for equivalents
of other kinds of non-classical logic, like Propositional Dynamic Logic or
Process Logic.
The following strict...
590.
Towards Programming in Default Logic
- Pawel Cholewinski
In this paper we describe a fragment of default logic suitable for encoding problems from other domains. We investigate a subclass of first order open default theories, which we call extensional default theories. This class of default theories allows easy and compact encodings of problems for experimenting with default reasoning systems. Because most existing systems for default reasoning assume that all input defaults are closed or propositional we show how to transform an extensional default theory to a closed first order default theory or a propositional default theory with same extensions. Finally, we present several encodings of known graph problems...
591.
Beyond Tamaki-Sato Style Unfold/Fold Transformations for Normal Logic Programs
- Abhik Roychoudhury; K. Narayan Kumar; C. R. Ramakrishnan; I.V. Ramakrishnan
Unfold/fold transformation systems for logic programs have been extensively investigated. Existing unfold/fold transformation systems for normal logic programs allow only Tamaki-Sato style folding using clauses from a previous program in the transformation sequence: i.e., they fold using a single, non-recursive clause. In this paper we present a transformation system that permits folding in the presence of recursion, disjunction, as well as negation. We show that the transformations are correct with respect to various semantics of negation including the well-founded model and stable model semantics.
592.
State-of-the-Art in CMOS Threshold-Logic VLSI Gate Implementations and Applications
- Peter Celinski; Sorin D. Cotofana; Jose F. Lopez; Said Al-Sarawi; Derek Abbott
In recent years, there has been renewed interest in Threshold Logic (TL), mainly as a result of the development of a number of successful implementations of TL gates in CMOS. This paper presents a summary of the recent developments in TL circuit design. High-performance TL gate circuit implementations are compared, and a number of their applications in computer arithmetic operations are reviewed. It is shown that the application of TL in computer arithmetic circuit design can yield designs with signi cantly reduced transistor count and area while at the same time reducing circuit delay and power dissipation when compared to...
593.
First-Order Logic with Two Variables and Unary Temporal Logic
We investigate the power of first-order logic with only two variables over
!-words and finite words, a logic denoted by FO
. We prove that FO
can
express precisely the same properties as linear temporal logic with only the
unary temporal operators: "next", "previously", "sometime in the future",
and "sometime in the past", a logic we denote by unary-TL. Moreover,
our translation from FO
to unary-TL converts every FO
formula to an
equivalent unary-TL formula that is at most exponentially larger, and whose
operator depth is at most twice the quantifier depth of the first-order formula.
594.
Some Pitfalls of Parallel Logic Programming
- Steven Prestwich
Logic programs are highly amenable to parallelization, and their level of abstraction relieves the programmer of many of the most difficult and errorprone details of parallel programming. However, tuning the performance of a parallel logic program is nontrivial. While working with programmers we noticed that they evolved strategies based on observed parallel performance.
595.
Improving Functional Logic Programs by Difference-Lists
- Elvira Albert; Cesar Ferri; Frank Steiner; German Vidal
. Modern multi-paradigm declarative languages integrate features from functional, logic, and concurrent programming. In this work, we consider the adaptation of the logic programming transformation based on the introduction of difference-lists to an integrated setting. Unfortunately, the use of difference-lists is impractical due to the absence of non-strict equality in lazy (call-by-name) languages. Despite all, we have developed a novel, stepwise transformation which achieves a similar effect over functional logic programs. We also show a simple and practical approach to incorporate the optimization into a real compiler. Finally, we have conducted a number of experiments which show the practicality of...
596.
Set-Term Unification in a Logic Database Language
- Seung Jin; Yiu-kai Ng
Deterministic, parallel set-term unification algorithms for high-order logic-based database languages, of which set terms have the commutative and idempotent properties, are lacking. As a result, an efficient inference mechanism that can be used to determine answers to queries of these database languages deterministically is nonexistent. To overcome these shortcomings, we propose a set-term unification algorithm for LDL=NR, a high-order logic database language. The proposed algorithm not only computes all generalized ground unifiers (ggu s ) of a given pair of set terms in LDL=NR without duplicates but also takes the advantage of existing multiple processors for computing all these unifiers...
597.
Set-Term Matching in a Logic Database language
- Seung Jin; Yiu-kai Ng
Existing set-term matching algorithms [AGS92] for logic-based database languages, of which set terms have the commutative and idempotent properties, have several problems: Given a pair of set terms, matchers can only be computed sequentially and duplicated matchers are generated. Hence, these algorithms cannot take the advantage of existing multiple processors for computing all matchers in parallel. Further, duplicated matchers are redundant and undesirable. In order to overcome these shortcomings, we propose an improved set-term matching algorithm for LDL=NR, a logic database language for nested relations, which generates non-redundant matchers for a given pair of set terms in parallel. The proposed...
598.
Constraint Logic Programming
- Francesca Rossi
Constraint logic programming (CLP) is a multidisciplinary research area which can be located between Artificial Intelligence, Operation Research, and Programming Languages, and has to do with modeling, solving, and programming real-life problems which can be described as a set of statements (the constraints) which describe some relationship between the problem's variables. This survey paper gives a brief introduction to C(L)P, presents a (necessarily partial) state of the art in CLP research and applications, points out some promising directions for future applications, and discusses how to cope with current research challenges.
599.
Compositional Logic Programming
- Trinity Term
Relational program derivation has gathered momentum over the last decade with
the development of many specification logics. However, before such relational specifications
can be executed in existing programming languages, they must be carefully
phrased to respect the evaluation order of the language. In turn, this requirement inhibits
the rapid prototyping of specifications in a relational notation. The aim of this
thesis is to bridge the gap between the methodology and practice of relational program
derivation by realising a compositional style of logic programming that permits
specifications to be phrased naturally and executed declaratively.
600.
Computational Aspects of Linear Logic
Linear logic was introduced by Girard in 1987 [30] both as a "logic behind logics", and as a "resource conscious logic". This thesis investigates computational aspects of linear logic. The main results of this work support the proposition that linear logic is a computational logic behind logics. This thesis augments the proof theoretic framework of linear logic by providing theorems such as permutability, impermutability, and cut-normalization with non-logical theories. On this expanded proof theoretic base, many complexity results are proved using a correspondence between proofs and computations. Among these results are the undecidability of propositional linear logic, the PSPACE-completeness of...
