The Journal of Functional and Logic Programming
- Ch. Brzoska,J. Darlington,Y. Guo,M. Hagiya,M. Hanus,T. Ida,J. Jaffar,B. Jayaraman
We address the type and effect inference in higher-order concurrent
functional programming languages `a la Concurrent ML. We present
three extensions of the type and effect discipline. First, the discipline
is extended to deal with infinite but recursive effects. Second, the
inferred effects are structured, i.e., we keep track of the structure of effects
(sequencing, choice, parallel composition, and recursion) instead
of using an AC1I (associative, commutative, unitary, and idempotent)
effect cumulation operator. Third, for the sake of flexibility, a subtyping
relation is considered on the type and effect algebras. This is
much more powerful than the classical subeffecting technique. This
is meant to avoid type mismatches that may arise...
Fat Estimation in Beef Ultrasound Images Using Texture and Adaptive Logic Networks
- James Darrell Mccauley,Brian R. Thane,A. Dale Whittaker
Overviews of Adaptive Logic Networks and co--
occurrence image texture are presented. These tools are
used for both prediction and classification of intramuscular
fat in beef from ultrasonic images of both live beef
animals and slaughtered carcasses. Results showed that
Adaptive Logic Networks perform better than any fat
prediction method for beef ultrasound images to date
and are a viable alternative to statistical techniques.
Keywords. Meat, Grading, Automation, Ultrasonic,
Instrument Grading of Beef
In the United States, beef carcasses are subjectively evaluated
by skilled human graders. One of the primary factors
in determining beef grades, and thus market value,
is the amount of intramuscular fat, or marbling. The
method used by human graders to...
Transformations of CLP Modules
- Sandro Etalle,Maurizio Gabbrielli
We propose a transformation system for Constraint Logic Programming (CLP) programs and modules.
The framework is inspired by the one of Tamaki and Sato for pure logic programs . However, the
use of CLP allows us to introduce some new operations such as splitting and constraint replacement.
We provide two sets of applicability conditions. The first one guarantees that the original and the
transformed programs have the same computational behaviour, in terms of answer constraints. The
second set contains more restrictive conditions that ensure compositionality: we prove that under these
conditions the original and the transformed modules have the same answer constraints also when they
Verification of Logic Programs and Imperative Programs
- Lee Naish
This paper explores the relationship between verification of logic programs and
imperative programs with the aim of uncovering the kinds of reasoning used
to construct logic programs. We discuss forward reasoning, such as that used
for verifying imperative programs using the inductive assertion method, and
backward reasoning, such as that used for verifying imperative programs using
subgoal induction and logic programs using consequence verification. We
argue that consequence verification is often inadequate for Prolog programs because
programmers make implicit assumptions about how procedures are called.
These assumptions can be made explicit using general type declarations.
Verification of logic programs with type declarations can be done in two steps.
Specification and Verification of Communicating Systems with Value Passing
- Dilian Borissov Gurov,C Dilian Borissov Gurov
The present Thesis addresses the problem of specification and verification of communicating
systems with value passing. We assume that such systems are described
in the well-known Calculus of Communicating Systems, or rather, in its value passing
version. As a specification language we propose an extension of the Modal ¯-Calculus,
a poly-modal first-order logic with recursion. For this logic we develop a proof system
for verifying judgements of the form b ` E : Phi where E is a sequential CCS term
and b is a Boolean assumption about the value variables occurring free in E and
Phi. Proofs conducted in this proof system follow the structure of...
Meta-Theory of Sequent-Style Calculi in Coq
- A. A. Adams
We describe a formalisation of proof theory about sequent-style calculi, based on
informal work in [DP96]. The formalisation uses de Bruijn nameless dummy variables
(also called de Bruijn indices) [dB72], and is performed within the proof assistant Coq
96]. We also present a description of some of the other possible approaches to
formal meta-theory, particularly an abstract named syntax and higher order abstract
Formal proof has developed into a significant area of mathematics and logic. Until recently,
however, such proofs have concentrated on proofs within logical systems, and meta-theoretic
work has continued to be done informally. Recent developments in proof assistants and automated
theorem provers have opened...
A Strong Correspondence between Description Logics and Open Logic Programming
- Kristof Van Belleghem,Marc Denecker,Danny De Schreye
This paper formally investigates the relationship between Open Logic Programming
(OLP) and Description Logics (DL). A description logic is designed
to represent two different forms of knowledge. A T-Box represents
definitional knowledge, i.e. definitions for a set of concepts. An A-Box
represents assertional knowledge about specific domain objects. OLP is
a declarative, terminological interpretation of the formalism of Abductive
Logic Programming. In this interpretation, an abductive logic program is
considered to consist of a T-Box providing definitions for non-abducible predicates
and an A-Box providing assertional knowledge in the form of first
order logic axioms. We define a provably correct mapping of DL theories
to open logic programs, and identify sublanguages...
DEE: a Tool for Genetic Tuning of Software Components on a Distributed Network of Workstations
- Ernesto Damiani,Gianni Degli Antoni,Andrea G. B. Tettamanzi
: This paper presents DEE, the Distributed Evolutionary
Engine, a complete framework for the off-line tuning of fuzzy-logic
based software components using parallel adaptation algorithms.
The system was implemented on a high-speed network of workstations
by means of a general-purpose task distribution tool. After
the description of DEE's architecture, the tuning of fuzzy software
components is discussed as an alternative to maintenance,
and some encouraging experimental results are described.
The idea of using evolutionary algorithms to tune parameters of fuzzy software
components is relatively recent. The first attempts in this direction were aimed
to the synthesis and optimization of fuzzy controllers (Karr 1991, Thrift 1991).
Besides control, another area of...
Learning from Paradox
The danger of paradoxes teaches us to check for consistency in (natural language) semantics. Paradoxes
typically involve an element of self-reference (the set-theoretic paradoxes) or an element of
self-reference combined with reference to truth (the semantic paradoxes). Self-reference need not be
vicious and talking about truth need not be glib, but linguists who allow self-reference or a truth
predicate in their representation languages should be aware of the dangers involved.
1 Russell's Paradox
The logical and semantical paradoxes that were discovered at the beginning of this century arose in a
context where formal languages were employed in a very loose sense. If Gottlob Frege is hailed in...
Logic Programming and Reasoning with Incomplete Information
- Michael Gelfond
The purpose of this paper is to expand the syntax and semantics
of logic programs and disjunctive databases to allow for the correct
representation of incomplete information in the presence of multiple
extensions. The language of logic programs with classical negation,
epistemic disjunction, and negation by failure is further expanded by
new modal operators K and M (where for the set of rules T and formula
F , KF stands for "F is known to be true by a reasoner with a set of
premises T " and MF means " F may be believed to be true" by the
same reasoner). Sets of rules in the extended...
First-class Polymorphism with Type Inference
- Mark P. Jones
Languages like ML and Haskell encourage the view of
values as first-class entities that can be passed as arguments
or results of functions, or stored as components
of data structures. The same languages offer parametric
polymorphism, which allows the use of values that
behave uniformly over a range of different types. But
the combination of these features is not supported---
polymorphic values are not first-class. This restriction
is sometimes attributed to the dependence of such languages
on type inference, in contrast to more expressive,
explicitly typed languages, like System F, that do support
This paper uses relationships between types and logic
to develop a type system, FCP, that supports first-class
A Linear Programming Approach for the Estimation of an Upper Bound on the Maximum Power of CMOS Circuits
- Etienne Jacobs,Michel Berkelaar
Maximum instantaneous power in VLSI circuits
is of great importance to the design of power
and ground lines in a VLSI circuit. Underestimating
the maximum instantaneous power greatly reduces the
circuits reliability. An accurate estimate of the maximum
instantaneous power is therefore needed. Unfortunately,
finding the input vectors which give the maximum
power consumption is a combinational problem.
An exhaustive search is very CPU-time intensive even
for small circuits with few primary inputs. We therefore
propose a novel linear programming approach, using
variables denoting switching scenarios, instead of
logic levels between possible switching events, to estimate
an upper bound on the maximum power consumption
in a CMOS circuit under an input vector change.
The Journal of Functional and Logic Programming
This paper proposes a number of models for integrating finitedomain
stochastic constraint solvers into constraint logic programming
systems to solve constraint-satisfaction problems e#ciently. Stochastic
solvers can solve hard constraint-satisfaction problems very e#-
ciently, and constraint logic programming allows heuristics and problem
breakdown to be encoded in the same language as the constraints;
hence their combination is attractive. Unfortunately, there is a mismatch
between the kind of information a stochastic solver provides
and that which a constraint logic programming system requires. We
study the semantic properties of the various models of constraint logic
programming systems that make use of stochastic solvers, and give
soundness and completeness results for their use. We describe...
The Arguments of Newly Invented Predicates in ILP
- Irene Stahl,Irene Weber
The task of predicate invention in Inductive Logic Programming is to extend
the hypothesis language with new predicates, in case the vocabulary
given initially is insufficient for the learning task. Introducing new predicates
involves searching for an appropriate argument structure.
In this paper we investigate the problem of choosing arguments for a new
predicate. We identify the relevant terms to be considered as arguments, and
propose methods to choose among them based on propositional minimisation.
The aim of inductive learning is to hypothesize a general rule from specific examples.
The success of this task strongly depends on the appropriate representation for both
examples and rules. A rule that...
Dynamic Control of Genetic Algorithms using Fuzzy Logic Techniques
- Michael A. Lee,Hideyuki Takagi
This paper proposes using fuzzy logic techniques to dynamically control parameter settings of genetic algorithms (GAs). We describe the Dynamic Parametric GA: a GA that uses a fuzzy knowledge-based system to control GA parameters. We then introduce a technique for automatically designing and tuning the fuzzy knowledge-base system using GAs. Results from initial experiments show a performance improvement over a simple static GA. One Dynamic Parametric GA system designed by our automatic method demonstrated improvement on an application not included in the design phase, which may indicate the general applicability of the Dynamic Parametric GA to a wide range of...
Fuzzy Logic Controllers Generated by Pseudo-Bacterial Genetic Algorithm with Adaptive Operator
- Norberto Eiji Nawa,Tomonori Hashiyama,Takeshi Furuhashi,Yoshiki Uchikawa
This paper presents a new genetic operator called
adaptive operator to improve local portions of chromosomes.
This new operator is implemented into PseudoBacterial
Genetic Algorithm (PBGA). The PBGA was
proposed by the authors as a new approach combining a
genetic algorithm (GA) with a local improvement mechanism
inspired by a process in bacterial genetics. The
PBGA was applied for the acquisition of fuzzy rules.
The aim of the newly introduced adaptive operator is to
improve the quality of the generated rules of the fuzzy
models, producing blocks of effective rules and more
compact models. The new operator adaptively decides
the division points of each chromosome for the bacterial
mutation and the cutting points...
Goal Oriented Equational Theorem Proving Using Team Work
- Jorg Denzinger,Matthias Fuchs
The team work method is a concept for distributing automated theorem
provers and so to activate several experts to work on a given problem. We have
implemented this for pure equational logic using the unfailing Knuth-Bendix
completion procedure as basic prover. In this paper we present three classes of
experts working in a goal oriented fashion. In general, goal oriented experts perform
their job "unfair" and so are often unable to solve a given problem alone.
However, as a team member in the team work method they perform highly efficient,
even in comparison with such respected provers as Otter 3.0 or REVEAL,
as we demonstrate by examples, some...
On Specification Frameworks and Deductive Synthesis of Logic Programs
- Kung-kiu Lau
this paper, we
take a closer look at such frameworks. We shall explain what they are, and how
they can be used to specify properties such as correctness and modularity (and
Moreover, we shall show that there is a close two-way relationship between
specification frameworks and deductive synthesis. In particular, a deductive synthesis
process can provide a useful feedback mechanism which can not only check
for desirable properties in the specification framework, but also improve the
framework (with regard to such properties) using the result of the synthesis.
In our approach to modularity, we borrow many of the basic ideas developed
in the algebraic approach (e.g. [6, 7,...
The BEAM: A first EAM Implementation
- V'itor Santos Costa,Ricardo Lopes
Logic programming provides a high-level view of programming, giving implementors a vast
latitude in what techniques to research towards obtaining the best performance for logic programs.
One of the holy grails of logic programming has been to design computational models that could
be executed efficiently and would allow for both a reduction of the search space and for exploiting
all the available parallelism in the application. These goals have motivated the design of the
Extended Andorra Model. We report on the design of a first implementation for the Extended
Andorra Model with Implicit Control, the BEAM.
Logic programming provides a high-level view of programming where programs...
Database Dependency Discovery: A Machine Learning Approach
- Peter A. Flach,Iztok Savnik
this paper are designed such that they can easily be generalised
to other kinds of dependencies.
Like in current approaches to computational induction such
as inductive logic programming, we distinguish between topdown
algorithms and bottom-up algorithms. In a top-down
approach, hypotheses are generated in a systematic way and
then tested against the given relation. In a bottom-up approach,
the relation is inspected in order to see what dependencies
it may satisfy or violate. We give algorithms for both
Keywords: Induction, attribute dependency, database reverse
engineering, data mining.