leff@smu.UUCP (Laurence Leff) (04/20/88)
This is our latest list of abstracts of SEKI REPORTS and SEKI WORKING PAPERS
for both 1986 and 1987.
PhD theses can be ordered at a nominal fee of US$ 10, SEKI REPORTS will cost
US$ 2, and SEKI WORKING PAPERS (which are mostly written in German) will cost
US$ 1.50, unless there is an exchange agreement.
There is, however, another way to obtain SRs and SWPs. You can subscribe to all
papers published during a year at a price of US$ 60. You will get each SR and
SWP immediately after its publication. The fee covers both postage and packing.
If you want to subscribe, please write (don't e-mail) and enclose a cheque.
The subscription will end after one year unless you explicitly order and pay
for another year.
If you want to order any publications, please enclose a cheque payable to
the university with the appropriate amount either in US$ or its equivalent in
your own currency. Cash is welcome, too.
Please, send your orders to the following address:
Scarlet Noekel
Universitaet Kaiserslautern
Fachbereich Informatik
Postfach 3049
6750 Kaiserslautern
West Germany
Phone: +49-631-205-2802
UUCP: ...!mcvax!unido!uklirb!scarlet
-------------------------------------------------------------------------
SEKI REPORTS SR-86-01 bis SR-86-20
SEKI-REPORT SR-86-01
K.-H.Blaesius
Consruction of Equality Graphs
Abstract: The theoretical and practical problems of equality rea-
soning in Automated Deduction are notorious. A new method is
presented to cope with the enormous search space that usually ar-
ises when equational axioms are present. Starting from an empty
graph a production system constructs graphs which represent solu-
tions for simpler problems defined by abstraction. These graphs
contain global information and are plans for guiding the search
for a proof of the original problem, represented in the final
graph. The construction of equality graphs is based on the idea
to search for the differences between two terms by seperating to-
plevel symbol and subterms of a functional term. The impact of
the explicit representation of information contained in the
inference system on the control of inferences is discussed. Fi-
nally the method is compared to other equality reasoning methods.
SEKI-REPORT-SR-86-02 Ch. Beierle, A. Voss
Specification, horizontal composition and parameterization of
algebraic implementations
Abstract: Loose specifications of abstract data types (ADTs) have
many nonisomorphic algebras as models. An implementation between
two loose specifications should therefore consider many abstrac-
tion functions together with their source and target algebras.
Just like specifications are stepwise refined to restrict their
class of models, implementations should be stepwise refinable to
restrict the class of abstraction functions. In this scenario
specifications and implementations can be developed interwovenly.
We suggest to have implementation specifications analo-
gously to loose ADT specifications: Implementations have signa-
tures, models, axioms and sentences thus constituting an institu-
tion. Implementation specifications are the theories of this in-
stitution and refinements between implementation specifications
are its theory morphisms.
In this framework, implementations between parameterized
specifications and horizontal composition of implementations turn
out to be special cases of the more powerful concept of
parameterized implementations, which allow to instantiate an im-
plementation by substituting a subimplementation by another im-
plementation.
SEKI-REPORT-SR-86-03 M. Reinfrank, M. Beetz, H. Freitag, J.
Klug
Kapri: A rule based non-monotonic inference engine with an in-
tegrated reason maintenance system
Abstract: KAPRI (Kaiserslautern Augmented Production Rule Inter-
preter) uses rules of the form if I unless I then I . For such a
rule to be fired, its monotonic if-antecedents are required to
match the current database, while none of its non-monotonic
unless-antecedents does. The current state of a KAPRI-system is
represented by a dependency network composed of assertions and
corresponding justifications for believing in them in terms of
belief respectively disbelief in other assertions. This network
is maintained by a reason maintenance system, KL-DNMS
(Kaiserslautern Dependency Network Management System), that re-
vises the current belief status with respect to every modifica-
tion due to the firing of a rule or to the addition/retraction of
a basic fact.
In the present paper, we describe a very simple first version of
KAPRI, and discuss some key issues that arise from augmenting
production rules by an UNLESS-part, and from integrating a pro-
duction rule-based inference engine with a reason-maintenance
system.
SEKI-REPORT-SR-86-04 H. Boley
A Relational/Functional Integration with valued Clauses
Abstract: The RELFUN programming language is introduced as an at-
tempt to integrate the capabilities of the relational and func-
tional styles. Definitions of functions and relations are speci-
fied uniformly by valued Horn clauses, where rules return the
value of their rightmost premise. Functional nestings are flat-
tened to relational conjunctions, using a purified version of
PROLOG's is-primitive. RELFUN functions may have non-ground argu-
ments, like relations, and/or return non-ground values; their in-
put and output arguments can be inverted like those of relations.
Higher-order functions are definable as (function-)valued
clauses, with funarg problems being avoided by the standard
renaming of clause variables. RELFUN's operational semantics is
specified as an abstract machine, which also yields its first
(e-mailable) FRANZ LISP implementation.
SEKI-REPORT-SR-86-05 H.-J. Buerckert
Some Relationships between Unification, Restricted Unification
and Matching
Abstract: We present restricted T-unification that is unification
of terms under a given equational theory T with the restriction
that not all variables are allowed to be substituted. Some rela-
tionships between restriced T-unification, unrestriced T-
unification and T-matching (one-sided T-unification) are esta-
blished. Our main result is that, in the case of an almost col-
lapse free equational theory the most general restricted unifiers
and for certain termpairs the most general matchers are also most
general unrestricted unifiers; this does not hold for more gen-
eral theories. Almost collapse free theories are theories, where
only terms starting with projection symbols may collapse (i.e. to
be T-equal) to variables.
SEKI-REPORT-SR-86-06 R. Goebel
Completion of Globally Finite Term Rewriting Systems for Induc-
tive Proofs
Abstract: The Knuth-Bendix Algorithm (KBA) is not able to com-
plete term rewriting systems with cyclic rules such as the commu-
tativity. This kind of rules cause cycles in a reduction chain.
This problem may be solved by an extension of the KBA for global-
ly finite term rewriting systems. For a globally finite term
rewriting system, cycles may occur in a reduction chain, but for
each term there is only a finite set of reductions. A confluent
and globally finite term rewriting sytem R provides a decision
procedure for equality induced by R: Two terms are equal iff
there is a common term in their reduction sets.
This extension requires new methods for testing the global fin-
iteness and a new confluence test, because local confluence does
not imply global confluence for globally finite relations. In
this paper we give a theoretical framework for this extension. We
will show how this theory can be applied to term rewriting sys-
tems, if we are mainly interested in the initial algebra which is
induced by the set of rules.
SEKI-REPORT-SR-86-07 M. Schmidt-Schauss
Unification Properties of Idempotent Semigroups
Abstract: Unification in free idempotent semigroups is of unifi-
cation type zero, i.e. there are unifiable terms s,t but there is
no minimal, complete set of unifiers for these two terms. Unifi-
cation in free idempotent semigroups is strongly complete, i.e.
the unification problem <x =AI t> is always solvable with unifier
{x , t}, even if x occurs in t.
We give a generalization of the usual unification hierarchy and
demonstrate that the number of independent unifiers in A+I-
unifier sets is not bounded.
It is known that there is a conditional, canonical term rewriting
system for idempotent semigroups. To strengthen this result, we
show that there can be no unconditional and finite rewriting sys-
tem.
SEKI-REPORT-SR-86-08 M. Schmidt-Schauss
Some Undecidable Classes of Clause Sets
Abstract: The undecidability of finitely generated stable transi-
tive relations on free terms is proved in an elementary way and
then used to show the undecidability of the implication A^B of
two clauses A and B. The implication is decidable in the case A
has at most two literals that are complementary unifinable after
renaming. Application of the undecidability of transitive rela-
tions yields more classes of clause sets that have an undecidable
satisfiability problem: clause sets consisting of two clauses
with two literals each (2-clauses) and in addition 2 ground un-
its, clause sets consisting of a single 3-clausse and arbitrarily
many (non-ground) units and clause sets conssting of a 4-clause
and arbitrarily many ground units. Finally we show the undecida-
bility of the so-called D-clause sets, where a D-clause is a
Horn-clause of the form
Q1(x1) Y<Y Qn(xn) ^ Qn+1(t) .
SEKI-REPORT-SR-86-09 W. Olthoff
The Augmentation of Object-Oriented Programming by Concepts of
Abstract Data Type Theory: The ModPascal Experiences
Abstract: Object-oriented programming and abstract data type
(ADT) theory have emerged from the same origin of computer sci-
ence: the inability during the early seventies to deal efficient-
ly with programming in-the-large. Each of the approaches has led
to significant practical and theoretical results resp. Neverthe-
less it is still unsatisfactory that the mutual influence up to
now seems to be limited to more or less syntactical issues (e.g.
the provision of packages, clusters, forms).
In this paper we report on the object-oriented language ModPascal
that was developed as part of the Integrated Software Development
and Verification (ISDV) Project.We show how the essence of con-
cepts of ADT theory as algebraic specifications, enrichments,
parameterized specifications or signature morphisms as well as
their semantics can be consistently integrated in an imperative
object-oriented language. Furthermore, as the experience of using
ModPascal as target language of the ISDV System has shown, we
claim that without similar support of theoretical concepts tech-
niques as formal specification of programs and algebraic verifi-
cation loose their power and even applicability.
SEKI-REPORT SR-86-10
Chr. Lingenfelder
Transformation of Refutation Graphs into Natural Deduction Proofs
Abstract: Most computer generated proofs are stated in abstract
representations not normally used by mathematicians. We describe
a procedure to transform proofs represented as abstract refuta-
tion graphs into natural deduction proofs. The emphasis of this
investigation is more on stylistic aspects rather than theoreti-
cal issues. In particular the topological properties of refuta-
tion graphs can be successfully exploited in order to obtain
structured proofs.
SEKI-REPORT SR-86-11
R. Socher
Verification of COBOL-Rrograms
Abstract: The use of COBOL for program verification leads to some
special problems enforcing the restriction of a verification sys-
tem to a small subset of the language. This report descibes the
language Ass Cobol, a subset of the COBOL standard from 1974. The
semantic of this language is given by translations of the
language into PASCAL statements. Based on this semantic, a system
of Hoare-style inference rules is constructed and its correctness
is shown.
Two examples demonstrate the complexity of the correctness proofs
even of small Ass Cobol programs.
SEKI-REPORT SR-86-12
(meanwhile published in the Springer Informatik Fachberichten No.
148)
Not available from us any more!
F. Puppe
Associative Diagnostic Problem Solving with the Expert System
Shell Med 2
Abstract: The motivation, the structure, the use and also the
restrictions of the expert system shell for classification prob-
lem solving are described. Its architecture is based on the in-
tegration of typical classification strategies including
hypothetico-deductive reasoning being complemented by standard-
ized preplanning of diagnostic tests, differential diagnosis,
separation of database and diagnostic reasoning, and the combina-
tion of several criteria for hypothesis evaluation.
The efficient implementation of these mechanisms is based
on the concentration of a small set of suspected hypotheses in
the working-memory and the aggregation of related symptoms to
questionsets providing an adequate abstraction level for
hypothetico-deductive reasoning. Criteria for evaluating hy-
potheses include categorial and probabilistic rules, a predispo-
sition score and an indicator in the value of a diagnosis for ex-
plaining symptoms. All rules can be qualified by exceptions. For
retracting premature conclusions, an efficient belief revision
algorithm is used. Its correctness depends on blocking circular
conclusions at run-time which is implemented in MED2. It is also
used for evaluating follow-up sessions in which the change of
symptoms with time yields additional diagnostic evidence.
Developing, changing and testing of a knowledge base are support-
ed by the knowledge-acquisition component, the use of which re-
quires no knowledge in programming languages, and by the explana-
tion component, which separates between a user and a knowledge-
engineer mode. Currently two major knowledge bases exist in a
medical and a technical domain. MED2 runs on various LISP-
dialects including COMMONLISP on the IBM-AT and has a size of
about 600 K byte.
SEKI-REPORT SR-86-13
Chr. Beierle, A.Voss
Hierarchical structures and dynamic parameterization without
parameters
Abstract: Hierarchical structuring and parameterization concepts
are investigated. It is argued that such concepts can be studied
independently of a particular domain of application and orthogo-
nally to the design of the +flat` objects. A dynamic parameteri-
zation concept which disposes of the static declaration of formal
parameters is proposed and realized in a hierarchy definition
language. The methods suggested are illustrated by applying them
to algebraic specifications, and it is shown how the approach ex-
tends the notion of an institution by a general structuring and
parameterization concept
SEKI-REPORT SR-86-14
Chr. Beierle, A. Voss
On implementation of loose abstract data type specifications and
their vertical composition
Abstract: In an approach for the implementation of loose abstract
data type specifications that completely distinguishes between
the syntactical level of specifications and the semantical level
of models, vertical implementation composition is defined compa-
tibly on both levels. Implementations have signatures, models and
sentences whrer the latter also include hidden components, which
allows for useful normal form results. We illustrate the stepwise
development of implementations as well as their composition by
some examples and describe the incorporation of the concept into
an integrated development and verification system.
SEKI-REPORT SR-86-15
Chr. Beierle, A. Voss
Stepwise development: Combinig axiomatic and algorithmic ap-
proaches in algebraic specifications
Abstract: Much of the software development activity can be car-
ried out using formal specifications that have a precise and well
defined semantics, making it possible to formally verify the
correctness of the development steps. In order to support this
claim we present an algebraic specification method that provides
both axiomatic and algorithmic techniques and illustrate it by
working through an example development. Our method is realized in
the specification development language ASPIK, which is a core
component of an integrated software development and verification
system. The semantics of ASPIK is based on the new notion of
canonical term functor which generalizes the notion of canonical
term algebra, and we show how this notion allows a uniform in-
tegration of axiomatic and algorithmic constraints.
SEKI-REPORT SR-86-16
A. Herold
Narrowing Techniques Applied to Idempotent Unification
Abstract: A complete unification algorithm for idempotent func-
tions is presented. This algorithm is derivated from the univer-
sal unification algorithm, which is based on the narrowing rela-
tion. First an improvement for the universal algorithm is shown.
Then these results are applied to the special case of idempotence
resulting in an idempotent algorithm. Finally several refinements
for this algorithm are proposed.
SEKI-REPORT SR-86-17
G. Smolka
Order-Sorted Horn Logic: Semantics and Deduction
Abstract: This paper presents a typed definite clause logic with
equality. The type structure accomodates subtypes and multiple
type declaration for functions and predicates. We show that the
semantic and deductive methods developed for untyped equational
logic genaralize smoothly to this framework.
SEKI-REPORT SR-86-18
R. Goebel
Ground Confluence
Abstract: In this paper we introduce a test for confluence on
ground terms. This test allows us to prove the ground cofluence
of term rewriting systems where the Knuth-Bendix Algorithm does
not terminate.
Ground Confluence of term rewriting systems is sufficient, if one
is interested in congruences on ground terms. This is for example
the case in the domain of inductive proofs or in the domain of
program synthesis.
SEKI-REPORT SR-86-19
J. Siekmann, P. Szabo
The Undecidability of the DA-Unification Problem
Abstract: We show that the DA-Unification problem is undecidable.
That is, given two binary function symbols v and , variables and
constants, it is undecidable if two terms built from these sym-
bols can be unified provided the following DA-axioms hold:
(x v y) z = (x z) v (y z)
x (y v z) = (x y) v (x z)
x v (y v z) = (x v y) v z
Two terms are DA-unifiable (i.e. an equation is solvable in DA)
if there exist terms to be substituted for their variables such
that the resulting terms are equal in the equational theory DA.
This is the smallest currently known axiomatic subset of
Hilbert's Tenth Problem for which an undecidabilty result has
been obtained.
SEKI-REPORT SR-86-20
H.-J. Buerkert, A. Herold and M. Schmidt-Schauss
On Equational Theories, Unification and Decidability
Abstract: The following classes of equational theories, which are
important in unification theory, are presented: permutative, fin-
ite, Noetherian, simple, almost collapse free, regular, and W-
free theories. The relationships between the particular theories
are shown and the connection between these classes and the unifi-
cation hierarchy is pointed out. We give an equational theory
that always has a minimal set of unifiers for single equations,
but there exists a system of two equations which has no set of
unifiers. This example suggests that the definition of the unifi-
cation type of an equational theory has to be changed. Further-
more we study the conditions, under which minimal sets of unif-
iers always exist.
Decidability results about the membership of equational
theories to the classes above are presented. It is proved that
Noetherianness, simplicity, almost collapse freeness and W-
freeness are undecidable. We show that it is not possible to de-
cide where a given equational theory resides in the unification
hierarchy and where in the matching hierarchy.
SEKI WORKING PAPER SWP-86-01 bis SWP-86-10
The SEKI Working Paper series was established in 1986.
SEKI-WORKING-PAPER SWP-86-01 (in German)
F. Puppe, H. Voss
Qualitative Modelle in wissensbasierten Systemen
Abstract: An overview on the representation and use of qualita-
tive models in knowledge based systems is presented. It is divid-
ed in two parts: first, we discuss several papers (CADUCEUS,
ABEL, Long's system, and Davis' system) using different kinds of
causal models.
In the second part, we describe important aspects of the underly-
ing methods, particularly the object-oriented and the process-
oriented approach. Special emphasis is given to constraint tech-
niques commonly used for implementation. Further topics include
representation methods for temporal and causal relations, the no-
tion of object states, the differnce between continuos and
discrete variables, and the necessity of hierarchies of models.
We close with an outlook on unsolved problems.
SEKI-WORKING-PAPER SWP-86-02 (in German)
H. W. Eiden, M. Linster
HIQUAL: Implementation of a System for Representation of
Time
and Causuality
Abstract: Hiqual is a language for representation and analysis of
modularly constructed hierachical physical or technical systems.
Models are the basic elements. They allow the cause-effect
description of elementary systems on both the causal and temporal
level.
Simple hierachical systems are described in aggregates. Aggre-
gates combine models on two levels of abstraction. More complex
hierarchies are described by means of combined aggregates.
The analysis of a model description generates a cyclic graph con-
taining all the possible behavioural sequences of the model.
Aggregates are checked to make sure that the different levels of
abstraction describe the same, but more or less abstract
behaviour. As every model may have an infinte number of
behavioural sequences, these tests are only executed for user
selected sequences.
The analysis is based upon Allen's temporal relations and rela-
tions among events belonging to different models and to find
dead-locks caused by inconsistencies.
The present paper describes the implementation and mentions those
problems that did not find a satisfactory solution, i.e. the
representation of inequalities and discontinuous values, and the
computational complexity of the analysis.
SEKI-WORKING-PAPER SWP-86-03 (in German)
M. Dahmen
Iterativer LISPLOG Interpreter - Implementierung, Doku-
mentation und Evaluation
Abstract: This paper discusses the interactive interpreter LISP-
LOG.2, which was developed from the earlier recursive version
LISPLOG.1. The goal of the development was to speed up the execu-
tion of LISPLOG programs. A comprision between the two LISPLOG
versions - given in chapter three - shows to what extent this
goal could be achieved.
The first chapter of this documentation of the main aspects of
LISPLOG.2. Since LISPLOG.2 was developed from LISPLOG.1 it may be
useful to consult the documentation of LISPLOG.1 too.
The appendices include the listing of the LISPLOG.2 interpreter
abd the programs used for the performance analysis.
SEKI-WORKING-PAPER SWP-86-04 (in German)
M. Lessel
micro-UNIXPERT Ein wissensbasiertes System zur Behandlung von
Problemen bei UNIX-Druckauftraegen
Abstact: micro-UNIXPERT (UNIXR - PERiphery - Tester) is an in-
teractive, knowledge-based diagnosis system for the treatment of
printer hardware faults and of other problems which can appear in
connection with printing (user errors and software faults).
If possible, the system both generates diagnosis and gives propo-
sals for clearing. The entire knowledge of micro-UNIXPERT con-
sists of a set of PROLOG-Like facts and rules.
The system is implemented in LISPLOG, a LISP/PROLOG integration
running in FRANZ LISP under the UNIX 4.2 BSD operating system on
a VAX 11/750.
After a general introduction into the problems of diagnosis sys-
tems and a discussion of the most important micro-UNIXPERT
features (knowledge acquisition, positive and negative facts,
user acceptance, inference mechanism), the method of operation of
the system is explained by giving full details of the LISPLOG im-
plementation.
SEKI-WORKING-PAPER SWP-86-05 (in German)
K. Hinkelmann
Uebersetzung von LISPLOG-Programmen nach CPROLOG
Abstract: A LISPLOG program is a set of horn clauses. Pure
PROLOG+s proof strategy is a kind of resolution. In LISPLOG, how-
ever, LISP by evaluating the LISP functions instead of using the
resolution theorem prover. To translate a LISPLOG program into
CPROLOG, these function applications have to be transformed into
applications of PROLOG relations. In order to prove these rela-
tions by resolution, new horn clauses have to be added to the da-
tabase. These new horn clauses are created from the definition of
the corresponding LISP function.
SEKI-WORKING-PAPER SWP-86-06 (in German)
Juergen Herr
Ein Ansatz fr einen LISPLOG Compiler mit LISP als Zielsprache
Abstract: This paper describes my work on compilation of
LISPLOGclauses into LISPfunctions and an improved runtimesystem
for LISPLOG, in which these functions will be interpreted. The
first part of this paper introduces and comments on the imple-
mented functions, while the reasons for fundamental design deci-
sions will be shown in the second part. Thus the first part is a
program documentation, whereas the second part gives more de-
tailed informations.
Furthermore the paper discusses in detail the question
whether it makes sense to use (portable) LISP as the target
language for a Hornclause compiler. This is the main point of the
second part of this paper, and I hope it will become apparent by
comparison with Warren+s abstract machine, that (portable) LISP
is not very suitable for this purpose.
SEKI-WORKING-PAPER SWP-86-07 (in German)
K. Noekel, R. Rehbold
SASL: Implementierung einer rein funktionalen Programmiersprache
mit
Lazy Evaluation
Abstract: This report presents an implementation of SASL in Lisp
which uses abstraction of variables and reduction of combinator
graphs. Following an introduction to SASL a section shows in de-
tail how SASL programs can be translated into compact combinator
graphs, with special emphasis on the methods used to deal with
local definitions, function definitions that spread over several
lines making use of pattern matching for case selection, and with
ZF-set notation. The second part of the report gives a detailed
account of the concrete implementation of an efficient algorithm
for the reduction of combinator graphs.
SEKI-WORKING-PAPER SWP-86-08
Harold Boley (Ed.)
A Bird+s-eye- View of LISPLOG:
The LISP/PROLOG Integration with Initial-cut Tools
Abstract: A combined LISP/PROLOG system was designed, implemented
and tested, via stepwise refinement of Kenneth M. Kahn+s opera-
tional LISP semantics for pure PROLOG.
LISPLOG.1 utilizes the representation of PROLOG terms as
LISP-S-expressions for two generalizations of Edinburgh PROLOG:
varying length structures, and goals with predicate variables. On
the other hand, a goto > while-like specialization is studied in
this language: the
cut > initial cut restriction, which improves both readability
and parallelization of PROLOG programs.
For accessing LISP from PROLOG, we permit LISP predicates
as goals, and LISP functions as right-hand sides of the is-
predicate.
In the other direction, the first n PROLOG solutions can be re-
turned as a LISP list.
LISPLOG.2 augments the trace and break tools already
available in LISPLOG.1 by an (initial) +cut-indicator+/+manual
cutter+ for making the cuts in the search tree observable and in-
teractive.
For improving efficiently, the originally recursive in-
terpreter is reformulated iteratively, the binding environment is
represented as an array structure, and the database is indexed by
predicates and arguments.
As the main application, LISPLOG runs a knowledge-based
system, m-UNIXPERT, for diagnosing printing problems.
SEKI-WORKING-PAPER SWP-86-09 (in German)
Franz Kammermeier
LISPLOG im Kontext anderer LISP/PROLOG-Vereinheitlichungen
Abstract: Since 1979 a lot of functional/relational languages
integrating LISP and PROLOG have been described in the litera-
ture. In this paper it is tried to find the position of LISPLOG
in the context of ten important other hybrids, which are mainly
LISP based, e.g. LOGLISP, LM-Prolog and Symbolics Prolog.
After a short introduction and a general view of these hybrids,
firstly the integration of programming styles is compared, namely
the correspondence of LISP/PROLOG data structures and the fa-
cilities to access one formalism from the other. Implementation
techniques of PROLOG interpreters, like implementation of con-
trol, representation of term instances and database indexing, are
examined in the second part, with the emphasis being on LISP as
the implementation language.The comparison is supplemented by a
short description of compilation techniques for PROLOG (in LISP)
used by compilers of the treated languages.
Finally, some conclusions for present and future improvements of
LISPLOG are outlined.
SEKI-WORKING-PAPER SWP-86-10 (in German)
Ansgar Bernardi
Ein Indexierungskonzept fr LISPLOG-Datenbasen
Abstract:
LISPLOG is a LISP/PROLOG integration explored at the
Universitaet Kaiserslautern.To improve the performance of
the LISPLOG interpreter, an indexing concept has been
developed and implemented. Higher efficiency is gained by
eliminating unnecessary unifications.
Matching clauses are selected using the predicate and one con-
stant atomic argument of the conclusion. A special combination of
shared lists and binary trees is maintained by the indexing pro-
cedure to make this selection rather fast.The user may optionally
specify the indexing argument; the default-argument is changeable
when installing the system. The indexing concept and the imple-
mented algorithms and data structures are fully described
in this paper, together with a
complete source-listing (FRANZ LISP) of the implementation.