Implementing Safety–Critical Systems in Prolog: Experiences from the R & D at Siemens

Karl Stroetmann, Thomas Glaß, and Martin Müller

Siemens AG, Corporate Research and Development, D–81730 Munich, Germany E-mail: Karl.Stroetmann@zfe.siemens.de

Abstract

This paper starts with a discussion of some experiences gained from the implementation of safety–critical systems in Prolog. We argue that the fact that Prolog is an untyped language has proved to be one of its drawbacks. In particular, this causes problems when Prolog is used to implement safety–critical systems. We describe a way of equipping Prolog with a type system that does not require any change in the underlying Prolog compiler. Furthermore, we show that once Prolog has been equipped with a type system further static checks become possible. These checks result in major improvements of maintainability and quality of Prolog programs. We have implemented a tool performing these checks and discuss first experiences.

1 Introduction

The programming language Prolog has been used for about ten years inside the Corporate Research and Development of Siemens. During this time we have been able to recognize the main pros and cons of Prolog. There were a number of projects which were particularly successful and whose success is, at least partly, due to the fact that Prolog has been chosen as the implementation language. Among others, the following projects have used Prolog as the implementation language:

• The circuit verification environment (CVE) [FSTW91, BFL^{+}94] is a tool that is used to verify circuit designs. It uses binary decision diagrams as its main data structure. Among other applications, this tool is currently used for the verification of hardware used in communication systems [BLPV95].

• The system verification environment (SVE) [FSS^{+}95] is a tool that has emerged from the CVE system. It is used to verify communication protocols implemented in SDL and control software for industrial automation.

• Furthermore, a tool has been implemented in Prolog whose purpose is the specification, validation, and synthesis of software for interlocking systems. The interlocking system is specified in an abstract language, proved correct with respect to specified properties, and finally compiled into a low–level program running on the appropriate hardware platform.

• While the tools described above deal only with systems that can be described as state–transition systems with a finite set of states, the tool Seduct [Str95] is a theorem prover for first order logic and can therefore be used to verify arbitrary systems. However, in contrast to SVE and CVE, Seduct is not an automatic tool.

The tools mentioned above employ formal mathematical methods to check properties of hardware or software systems. Therefore, in all of these systems mathematical formulas play an important role. Obviously, Prolog terms are well–suited to represent these formulas. Furthermore, the matching facility of Prolog has proved to be a convenient means to implement programs that manipulate formulas.

However, the use of Prolog in these projects led to a major problem. The reason is the following: One major common feature of the systems described above is that the corresponding applications are, at least potentially, safety critical. As soon as software tools are used to prove safety–critical properties of systems or automatically generate code for safety–critical applications the quality of the tools becomes a matter of serious concern.

It was in this context that one of the major shortcomings of Prolog was recognized: Prolog is an untyped language. It is well–known that programs written in a strongly typed language are, in general, more reliable than programs written in an untyped language. Therefore various standards for the implementation of safety critical systems actually require the use of a typed programming language, cf. [din92]. Fortunately, the lack of types in Prolog is more of an historical accident than a feature inherent in logic programming. As a matter of fact, several typed logic programming languages have been proposed recently, for example Protos–L [Bei95a], Gödel [HL94], or Mercury [SHC95]. However, none of these proposals has reached the maturity needed in industrial applications. In particular, there are no commercially supported typed logic programming languages available that can be viewed as extensions of Prolog. Therefore, we decided to design a type system on top of Prolog and to build a type checker supporting this type system.

After the first version of this type checker had been implemented it became obvious that, since Prolog is a declarative language, a number of further properties of Prolog programs can be checked automatically by using formal methods. In particular, it is possible to automatically check the completeness and termination of programs which satisfy properly defined coding standards. These checks have been implemented on top of a type checker in a tool called Pan [SGM96].

The next section will present details of our type system. Section 3 discusses the notion of completeness and how it can be checked automatically. In Section 4 we describe how to ensure the termination of Prolog programs. Section 5 sketches a possible future extensions of Pan: the verification of invariants. Section 6 concludes the paper by discussing the results obtained so far.

2 Adding a Type System to Prolog

In this section we briefly present the type system implemented in Pan. After describing it from a user’s point of view we will discuss some of the theoretical issues concerning the implementation of this type system.

2.1 The Type System of Pan

When designing our type system we had to obey the following constraint: We wanted to be able to use this system as a supplement to an existing Prolog system. In particular, we wanted to avoid any change of the logic programming language Prolog. The reason is that, when developing safety critical systems, the software tools used have to be commercially supported, mature, and tested in a large number of application. Therefore, developing a new logic programming language or using any of the possible successors of Prolog currently developed at universities was not an option.

Since we were not allowed to change the Prolog system, we decided to add the type information in the form of special comments, e.g., the signature for the predicate append/3 takes the following form:

  %# predicate: append( + list(T), + list(T), - list(T) ).

This line is hidden from the Prolog interpreter since it starts with the comment character “%”. The following character “#” identifies the line as an input to Pan. The keyword “predicate” determines the line to be a signature definition. A signature definition consists of two parts, mode information and type information. Modes are specified by assigning the symbols “+” or “-” to the different argument positions of a predicate denoting input arguments and output arguments, respectively. In the example above, the first two arguments are specified as input arguments and the last argument as an output argument. Besides the mode information, a signature definition contains type information. In the example above, the type list(T) is associated with each of the arguments of append/3. The general form of a signature definition for a predicate p/n is as follows:

      %# predicate: p( m_{1}τ_{1}, · · ·, m_{n}τ_{n} ).

Here, for i = 1, ⋯, n we have m_{i} ∈ {+, -}, while τ_{i} is a type. We will discuss how to define types later in this section. For the moment we view types as names for sets of Prolog terms. With this interpretation a program is considered well–typed if the following holds for all calls of predicates:

• If the ith argument of the predicate p/n is specified as an input argument of type τ_{i}, i.e., if m_{i} = +, then for every call p(t_{1}, ⋯, t_{n}) of p/n the term t_{i} is an element of τ_{i}, i.e., t_{i} ∈ τ_{i} holds.

• If the ith argument of the predicate p/n is specified as an output argument of type τ_{i}, i.e., if m_{i} = -, then for every successful call p(t_{1}, ⋯, t_{n}) of p/n the term t_{i} is instantiated to an element of τ_{i}, i.e., after the call t_{i} ∈ τ_{i} holds.

The type system presented up to now does not contain any feature distinguishing it from the various type systems that have been proposed in the literature [AL94, Bei95a, Bei95b, BLR92, HT92, Pfe92, SHC95]. The important differences to other type systems become apparent when we discuss the way types can be defined with Pan. Basically, there are two possibilities. First, a type can be defined via a recursive equation. As an example, the polymorphic type list(T) used above is defined as

  %# list(T) := '[]' + '.'( T, list(T) ).

Here T is a type parameter that can be instantiated later. For example, given the type definition of list(T), we have the types list(int) and list(atom) at our disposal. This approach is similar to a type definition as, e.g., in Gödel [HL94]. However, using this kind of type definition only types with a finite set of different constructors can be defined. This causes problems when types that extend predefined types like, e.g., the type atom of all Prolog atoms, need to be considered. For example, with the scheme of recursive equations it is not possible to define a type regexp that includes the set of all characters, i.e., all Prolog atoms of length 1, and, furthermore, is closed under the constructors star/1, cat/2, and or/1. An inductive definition of the type regexp can be given as follows:

1. Every character is an element of type regexp.

2. If r is an element of type regexp, then the term star(r) is an element of type

     regexp.

3. If r_{1}, r_{2} are elements of type regexp, then the terms cat(r_{1}, r_{2}) and or(r_{1}, r_{2}) are elements of type regexp.

Since the type regexp contains an infinite number of constructors, it can not be be defined via a recursive equation. After all, a recursive equation would have to list all of the constructors explicitly. However, the type regexp is a natural representation for regular expressions, where for any regular expressions r, r_{1}, and r_{2} the term star(r) denotes the Kleene closure r^{∗}, cat(r_{1}, r_{2}) denotes the concatenation r_{1}r_{2} of r_{1} and r_{2}, and or(r_{1}, r_{2}) denotes the alternative r_{1}|r_{2}. With Pan the type regexp can be defined as follows:

  %# regexp extends atom by
  %#                star( regexp ) +
  %#                cat( regexp, regexp ) +
  %#                or( regexp, regexp ).

Of course, it could be argued that instead of using regexp the following alternative could be defined via a recursive equation:

  %# regexp2  :=     char( atom ) +
  %#                 star( regexp2 ) +
  %#                 cat( regexp2, regexp2 ) +
  %#                 or( regexp2, regexp2 ).

The problem with this solution is that, first, regexp2 denotes a different set of terms than regexp does. Changing the type definition is only applicable if the user has the freedom to design the types himself. Certain types used with the builtin predicates of Prolog according to the ISO–standard [DEDC96], however, can not be described in this way. Secondly, when using type definitions like the one for regexp2, programs soon get cluttered with unnecessary wrappers that render the resulting programs both inefficient and unreadable.

The definition of regexp given above turns atom into a subtype of regexp. Therefore, our type system has to support parametric polymorphism and inclusion polymorphism. We will discuss this matter further in the next subsection.

Up to now we have described our type system as an extensional type system where a type is identified with the set of its elements. Actually, this is an oversimplification. We have found a name based type system more useful. With the type system of Pan it is possible to have two different types that denote the same set of elements. For example, it is possible to define the following types:

   %# first name == atom.
   %# last name == atom.

Then, extensionally, first name and last name both denote the set of all Prolog atoms. However, Pan is still able to detect an inconsistency if a term representing a data object of type first name is wrongly used as a data object of type last name. With this feature of Pan it is, in particular, possible to find intricate type errors that can not be discovered by a system employing run time type checking.

2.2 Theoretical Considerations

Adding types to Prolog is not a new idea. In fact, one of the first proposals [Bru82] had the same motivation for adding types to Prolog as we have. Although slightly out of date, a good overview of the different type systems that have been proposed for logic programming is given in the collection of Pfenning [Pfe92]. More recent views on types in logic programming are given in [BLR92, AL94] and [Bei95a]. Unfortunately, as it stands none of the type systems proposed so far in the literature is really satisfactory. The reason is that none of them is able to express the signatures of the builtin predicates of Prolog according to the ISO–Standard.

The issue one has to resolve when designing a type system is that, in general, there is a tradeoff between expressiveness and computational complexity. Regarding expressiveness, it is generally accepted that a type system should provide polymorphic polymorphism. However, as we have pointed out in the last subsection, in order to be applicable to Prolog a type system has to provide inclusion polymorphism, too. In fact, there have been several proposals for a type system providing both, inclusion polymorphism and parametric polymorphism, the latest being [Bei95b], which builds on [HT92]. In these proposals, however, the integration of parametric polymorphism and inclusion polymorphism is not satisfactory since subtype relations of the form

K(σ_{1}, ⋯, σ_{m}) ≤ L(τ_{1}, ⋯, τ_{n}) can only hold if either K = L or m = n = 0. In practical applications we have found it of crucial importance to have a type term consisting of the set of all terms at our disposal such that

K(σ_{1}, ⋯, σ_{m}) ≤ term

holds for all type constructors K/m. A type system which improves the integration of parametric and inclusion polymorphism has been described in [SG95].

On the positive side, this type system provides the level of expressiveness that is needed in order to deal with the types which naturally arise when programming in Prolog. On the negative side, however, it is an open issue whether well–typedness of programs is decidable. This has not prevented us from implementing a strong heuristic that so far has dealt with all type–checking problems occurring in practice satisfactorily. Although this is not satisfying from a theoretical point of view, it has proved to be very useful in practice.

3 Completeness

Typical errors in Prolog programming show up when a predicate that should have succeeded in computing an instantiation of a goal simply fails and returns no. Since the answer no provides no hint for the cause of the error, these errors are frustrating and quite often time consuming to correct. After all, the error can be anywhere in the program. If there is no specification whether predicates are allowed to fail or not, then tracking down the error with a debugger can be quite involved.

Fortunately, once a type system has been implemented, checking whether a predicate can fail or always produces a solution becomes feasible. Although this question is not decidable in general we have stated sufficient conditions that guarantee that every type correct call of a predicate produces a solution. These conditions are decidable and, furthermore, general enough to be applicable to most Prolog programs. In order to give the reader a rough idea we present a simple example. We will define a type prop intended to represent propositional formulas via the following type definition:

  %# prop  :=  var( atom ) +
  %#           not( prop ) +
  %#           or( prop, prop ) +
  %#           and( prop, prop ).

With this type definition, the type prop consists of all terms of the form var(Atom) where Atom is a Prolog atom and is furthermore closed under application of not/1, or/2, and and/2. The terms of the form var(Atom) denote propositional variables. For example,

   or( var(x), not( var(x) ) )

is a simple Prolog term of type prop representing the propositional formula

x ∨ ¬x.

It is well known that propositional formulas can be rewritten into negation normal form by pushing negations inside, i.e., in order to compute the negation normal form we have to use the deMorgan laws:

¬(x ∧ y) ↔ ¬x ∨ ¬y,
¬(x ∨ y) ↔ ¬x ∧ ¬y.

Therefore, a first step towards a program that performs these transformations could be:

  %# predicate: nnf( + prop, - prop ) never_fails.
  nnf( var( Atom ), var( Atom ) ) :-
          !.
  nnf( not( var( Atom ) ), not( var( Atom ) ) ) :-
          !.
  nnf( not( or( P1, P2 ) ), and( Not_P1, Not_P2 ) ) :-
          !,
          nnf( not( P1 ), Not_P1 ),

nnf( not( P2 ), Not_P2 ).
nnf( not( and( P1, P2 ) ), or( Not_P1, Not_P2 ) ) :-
!,
nnf( not( P1 ), Not_P1 ),
nnf( not( P2 ), Not_P2 ).
nnf( or( P1, P2 ), or( P1_NNF, P2_NNF ) ) :-
!,
nnf( P1, P1_NNF ),
nnf( P2, P2_NNF ).
nnf( and( P1, P2 ), and( P1_NNF, P2_NNF ) ) :-
!,
nnf( P1, P1_NNF ),
nnf( P2, P2_NNF ).

However, Pan produces the following error message:

nnf.pro:1: incompleteness: nnf(not(not(P9)),_)

which point out that the case nnf( not( not( P ) ), ) is not dealt with. The trivial rule

¬¬x ↔ x

is not included in the program. The implementation of nnf/2 can be completed by adding the clause:

nnf( not( not( P ) ), P_NNF ) :-
!,
nnf( P, P_NNF ).

If we add this clause, Pan is able to show that every call of the form

nnf( P, N )

with P bound to a term of type prop and N a free Prolog variable terminates successfully.

It turns out that the idea underlying completeness checking of functions can be extended to predicates that are used as tests, i.e., predicates that are intended to fail in certain situations. Of course, in this case the implicit use of “negations as failure” is not allowed and has to be replaced by the notion of explicit failure. With this restriction, e.g., an implementation of the predicate member chk/2 checking for membership in a list has the following form:

%# test: member_chk( + list( T ), + T ) is_complete.
member_chk( [ X | Xs ], Y ) :-
X == Y,
!.

  member_chk( [ X | Xs ], Y ) :-
     X \== Y,
     !,
     member_chk( Xs, Y ).
  member_chk( [], _) :-
     !,
     fail.

The last clause has to be added to justify the attribute is complete. Otherwise it would be impossible to distinguish between failures that are actually intended by the programmer and those failures that are considered to be errors. Our experience is that formulating explicit failure conditions, although producing programs that are slightly longer, increases the readability of programs considerably.

Of course, we do not want to ban the concept of “negation as failure” all together. It is an option to classify predicates as is complete or never fails. The use of “negation as failure” is only prohibited for predicates classified in this way. As an example, it is still possible to have a database of facts and corresponding predicates that are classified neither as never fails nor as is complete. The paradigm of “negation as failure” can still be used for these predicates.

There is a further benefit when annotating predicates with the attributes is complete or never fails. We can guarantee that, provided certain restrictions concerning the use of the cut operator “!” are adhered to, the resulting programs have a declarative semantics that is equivalent to their operational semantics. The details of this declarative semantics are given in the paper [SG96]. The main point in this paper is a simple declarative interpretation to a restricted use of the cut operator. It is shown that a clause of the form

p(s) :- B_{1},!, B_{2}.

has the declarative semantics

B_{1} → (p(s) ↔ ∃u.B_{2})

where u is the tuple of all variables that are local to B_{2}, i.e., those variables of B_{2} which occur neither in B_{1}, nor in s. This result allows a functional programming style in Prolog without leaving the realm of declarativeness. This had been previously considered impossible for the following reason: The cut operator destroys the conventional declarative semantics. On the other hand, when using a functional programming style, the cut is necessary in order to suppress backtracking.

We conclude this section by comparing our approach with similar work described in the literature. The idea of checking the completeness of specifications that are given as conditional equations has been around for some years, cf. [BR91]. Using the semantics given in [SG96], Prolog programs can be transformed into conditional equations and checked for completeness. On the surface, checking completeness is akin to the check of determinism in the Mercury compiler [HSC96]. While the techniques used there seem to be quite different from ours, the experiences are the same: Analyzing the completeness of a program increases its maintainability by an order of magnitude.

4 Termination

A further property that can be checked with Pan is the termination of programs. Of course, it is well–known that this property is undecidable in general. However, it is possible to formulate sufficient conditions that guarantee termination. With our system, in order to check the termination of a program, the user has to specify predicate norms and dependency relations to be explained below. Once the predicate norm and the dependency relations are given, the question of termination can essentially be reduced to an integer programming problem. The theory behind our implementation is described in [Mül95] and builds upon [GP92] and [Wal90].

Basically, a predicate norm specifies an argument of a given predicate whose size is supposed to decrease for recursive calls of this predicate. A dependency relation specifies dependencies between the sizes of the arguments of a given predicate. This is most easily explained by means of an example. Consider the following version of the quicksort algorithm in Prolog.

  %# function: qs( + int*, - int* ) never_fails.
  qs( [ X | Xs ], Sorted ) :-
        split( X, Xs, Small, Big ),
        qs( Small, Small_Sorted ),
        qs( Big, Big_Sorted ),
        append( Small_Sorted, [ X | Big_Sorted ], Sorted ).
  qs( [], [] ).
  %# function: split( + int, + int*, - int*, - int* ) never_fails.

The implementation of split/4 is not given here. The call split(X, Xs, Small, Big) splits the list Xs into the parts Small and Big, where Small contains all those elements of Xs that are less than the pivot element X, while Big contains the remaining elements.

The predicate qs/2 terminates since the length of the first argument decreases for recursive calls. This is expressed by the predicate norm

  %# pnorm: | qs( L, S ) | = | L |.

In order to prove the termination of qs/2 we need to know how the arguments Small and Big of the recursive calls of qs/2 are related to the input argument [X|Xs] of qs/2. In the program, both Small and Big are computed from Xs via the predicate split/4. The dependency relation

  %# dependency( split( X, Xs, Small, Big ) ):
  %#           | Small | + | Big | =< | Xs |.

of the predicate split/4 specifies that the combined size of Small and Big is indeed less than or equal to the size of Xs and therefore strictly less than the size of [X|Xs]. Therefore qs/2 terminates.

Of course, in practice the question of termination is much more involved than in the trivial example presented here. We refer the reader interested in more details to the papers cited above.

5 Verification

For the future, we intend to investigate on further properties that can be verified automatically. Preliminary experiences with a theorem prover currently developed indicate that it should be possible to verify invariants that satisfy certain syntactic restrictions. For example, consider the following program.

  %# function: merge( + int*, + int*, - int* ) never_fails.
  merge( [], L, L ) :-
          !.
  merge( L, [], L ) :-
          !.
  merge( [ X | Xs ], [ Y | Ys ], [ X | Merge ] ) :-
          X =< Y,
          !,
          merge( Xs, [ Y | Ys ], Merge ).
  merge( [ X | Xs ], [ Y | Ys ], [ Y | Merge ] ) :-
          X > Y,
          !,
          merge( [ X | Xs ], Ys, Merge ).

The predicate merge/3 is intended to merge its two input arguments in such a way that the resulting list is ordered provided that the input arguments are lists that are ordered. Let us assume that ord(L) is true if and only if L is a list that is ordered. If we think of the predicate merge/3 as coding a binary function merge(·, ·), then this function can be specified as follows:

ord(merge(L_{1}, L_{2})) ↔ ord(L_{1}) ∧ ord(L_{2}). (∗)

With current technology in automatic theorem proving it is possible to automatically verify that the implementation given above does indeed satisfy the specified property. In order to carry out this verification the program has to be transformed into a set of conditional equations according to the semantics given in [SG96]. These equations can then be shown to imply the property (∗). Moreover, if the program implementing merge/3 is changed such that the property given above becomes false, it is possible to automatically construct a counter example [Eng96].

Nevertheless, a word of caution is appropriate. In order to verify properties of a top level predicate it is necessary to find corresponding properties of all the predicates used in its implementation. Finding these properties may turn out so difficult and time consuming that a complete verification still remains infeasible on economic grounds. However, we believe that even if only some low level predicates can be verified, the resulting increase in quality might well be worth the effort.

6 Conclusion

In this paper, we have sketched a method that is capable to find a significant class of errors in Prolog programs via improved static analysis techniques. At the heart of the method lies the application of formal methods. While previous approaches to apply formal methods to software development have not been able to offer an increase in productivity, this is not the case for our approach. In contrast to other approaches which aimed at a complete formal verification we intend to verify only those properties where an automatic verification is feasible. Our main focus has not been a proof of correctness but rather the uncovering of errors.

The method described in this paper has been implemented in a tool called Pan. Using this tool we have found that even a type system alone significantly increases the productivity of software development in Prolog. However, once Prolog programs are typed, checking further properties of programs like completeness and termination becomes feasible. Although the programmer has to specify the types as well as certain other properties in order to use the full power of Pan, the experience gained so far shows that there is ample reward for this extra effort, especially in the maintenance of programs. The reason for the latter is that maintaining a program often involves changing data types. Pan readily finds all those predicates whose definitions have to be changed in turn. Another interesting observation is that, as soon as the complexity of the data types used exceeds a certain limit, programmers tend to forget cases. Often, this does not result in an immediate error on simple test examples since the same cases that were overlooked in the program will be overlooked when designing the test cases.

Actually, when we finished the first prototype of Pan, we were quite surprised when Pan spotted errors in programs that had already been running for some time without showing any errors and whose correctness therefore had been taken for granted. With the present state of the art, software that is both complex and error free is a dangerous illusion. Therefore, we recommend that when implementing safety–critical systems, one should try to use formal methods to uncover as many errors as possible. With the approach sketched in this paper this seems to be possible without increasing the price of software development. Quite on the contrary, the use of certain formal methods can reduce the cost of software significantly since it is possible to spot errors both early and automatically. Acknowledgments. The authors would like to thank Dr. Gerd Venzl for a number of helpful discussions on the subject of this work. Furthermore, we thank him for carefully proofreading earlier versions of this paper.

References

[AL94] Alexander Aiken and T. K. Lakshman. Directional type checking of logic programs. In Baudouin Le Charlier, editor, Static Analysis, volume 864 of Lecture Notes in Computer Science, pages 43–60. Springer–Verlag, 1994.

[Apt92] Krzysztof R. Apt, editor. Logic Programming. The MIT Press, 1992.

[Bei95a] C. Beierle. Concepts, implementation, and applications of a typed logic programming language. In Beierle and Plümer [BP95], chapter 5, pages 139–167.

[Bei95b] Christoph Beierle. Type inferencing for polymorphic order-sorted logic programs. In Leon Sterling, editor, Proceedings of the 1995 International Conference on Logic Programming. MIT Press, 1995.

[BFL^{+}94] Jörg Bormann, Thomas Filkorn, Jörg Lohse, Michael Payer, Gerd Venzl, and Peter Warkentin. CVE: an industrial formal verification environment. Technical report, Siemens AG, Corporate R & D, D-81730 Munich, Germany, 1994.

[BLPV95] Jörg Bormann, Jörg Lohse, Michael Payer, and Gerd Venzl. Model checking in industrial hardware design. In Proceedings of the 32nd Design Automation Conference, pages 298–303, 1995.

[BLR92] François Bronsard, T. K. Lakshman, and Uday S. Reddy. A framework of directionality for proving termination of logic programs. In Apt [Apt92], pages 321–335.

[BP95] C. Beierle and L. Plümer, editors. Logic Programming: Formal Methods and Practical Applications. Studies in Computer Science and Artificial Intelligence. Elsevier Science B.V./North-Holland, Amsterdam, Holland, 1995.

[BR91] Wadoud Bousdira and Jean-Luc Rémy. On sufficient completeness of conditional specifications. In Stéphane Kaplan and Mitsuhiro Okada, editors, Conditional and Typed Rewriting Systems, 2nd International Workshop, LNCS 516, pages 272–286. Springer-Verlag, 1991.

[Bru82] Maurice Bruynooghe. Adding redundancy to obtain more reliable and more readable Prolog programs. In Proceedings of the First International Logic Programming Conference, pages 129–133, 1982.

[DEDC96] P. Deransart, A. A. Ed-Dbali, and L. Cervoni. Prolog: The Standard. Springer-Verlag, 1996.

[din92] Software für Computer in der Anwendung industrieller Sicherheitssysteme. DIN IEC 65A(Sec) 122, 1992.

[Eng96] Andrea Engelhardt. Automatisches Beweisen und Erzeugung von Gegenbeispielen in induktiven Theorien. Masters thesis, Ludwig-Maximilians-Universität München, May 1996.

[FSS^{+}95] Th. Filkorn, H.-A. Schneider, A. Scholz, A. Strasser, and P. Warkentin. SVE: Users’ guide. Technical report, Siemens AG, Corporate R & D, D-81730 Munich, Germany, 1995.

[FSTW91] Thomas Filkorn, Richard Schmid, Erik Tidén, and Peter Warkentin. Experiences from a large industrial circuit design application. In Vijay Saraswat and Kazunori Ueda, editors, Logic Programming, Proceedings of the 1991 International Symposium, pages 581–595, San Diego, USA, 1991. The MIT Press.

[GP92] Gerhard Gröger and Lutz Plümer. Handling of mutual recursion in automatic termination proofs for logic programs. In Apt [Apt92], pages 336–350.

[HL94] P.M. Hill and J.W. Lloyd. The Gödel Programming Language. MIT Press, 1994.

[HSC96] Fergus Henderson, Zoltan Somogyi, and Thomas Conway. Determinism analysis in the mercury compiler. In Proceedings of the Australian Computer Science Conference, pages 337–346, Melbourne, Australia, January 1996.

[HT92] P. M. Hill and R. W. Topor. A semantics for typed logic programs. In Pfenning [Pfe92], pages 1–62.

[Mül95] Martin Müller. Automatisierbare Terminierungsnachweise von Prolog–Programmen. Master’s thesis, Universität Marburg, 1995. This paper is available

at: http://www.mathematik.uni-marburg.de/~mueller/termnach.ps.

[Pfe92] Frank Pfenning, editor. Types in Logic Programming. The MIT Press, 1992.

[SG95] Karl Stroetmann and Thomas Glaß. A semantics for types in prolog: The type system of pan version 2.0. Technical report, Siemens AG, ZFE T SE 1, 81730 München, Germany, 1995.

[SG96] Karl Stroetmann and Thomas Glaß. A declarative semantics for the prolog cut operator. In Peter Schröder-Heister, editor, Proceedings of the Workshop on Extensions of Logic Programming, Lecture Notes in Computer Science. Springer Verlag, 1996. To appear.

[SGM96] Karl Stroetmann, Thomas Glaß, and Martin Müller. Pan V2.0 — a tutorial. Technical report, Siemens AG, Corporate Research and Development, D-81730 Munich, Germany, 1996.

[SHC95] Zoltan Somogyi, Fergus Henderson, and Thomas Conway. Logic programming for the real world. In Donald A. Smith, Olivier Ridoux, and Peter Van Roy, editors, Proceedings of the Workshop Visions for the Future of Logic Programming: Laying the Foundations for a Modern Successor to Prolog, pages 83–94, 1995. The Proceedings of this workshop are available at:

ftp://ps-ftp.dfki.uni-sb.de/pub/ILPS95-FutureLP/.

[Str95] Karl Stroetmann. Seduct — a proof compiler for first order logic. In Manfred Broy and Stefan Jänichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software, volume 1009 of Lecture Notes in Computer Science, pages 299–316. Springer Verlag, 1995.

[Wal90] Christoph Walther. Automatisierung von Terminierungsbeweisen. Vieweg, Braunschweig, Germany, 1990.