"Our website has moved from Amsterdam to Leuven (thanks Eric Monfroy, Sebastian Brand and Krzysz Apt for its initial setup and for all these years of maintenance, thanks Bart Demoen and his students Tom Schrijvers and Remko Tronçon for the transfer and enhancements, and thanks also to Danny Penders and Sandro Etalle for the web pages of our Newsletter!)."

The 9th Prolog Programming Contest took place in Mumbay, on the 9th of December 2003, at the occasion of ICLP'04. The help we got for organizing it, was overwhelming: Anbu and Sachin provided technical support and installed the software, RedHat India provided excellent Dell machinery, Shyam (general chair) and Catuscia (program chair) provided an superb slot in the program and all we needed to top it off was ... contestants!

You can find the problems on http://www.cs.kuleuven.ac.be/~bmd/PrologProgrammingContests/ and try them for yourself. When we were making them up, we already thought the problems would be not too difficult. But problems can be deceiving: at some point Bart came up with a problem from a graph theory book and it could be solved by finding two complete subgraphs with exactly one node in common. Bart wrote a program for that in about 12 minutes, with only 6 predicates and 35 lines of code, and he was very proud of that. When he send the problem to Phuong-Lan, she replied almost instantly with a program that solves the same problem, but with just one predicate and only seven lines of code ... she had dismissed the graph context completely, and her solution was obviously correct. You are curious now: it's the "cheater" problem. During the contest (and also its web version) about half of the teams solved it like Bart, about half like Phuong-Lan!

• 3 teams submitted 2 correct solutions: a couple of years ago, there was no winner in this contest because nobody had 2 correct !
• 3 teams submitted 3 correct solutions: in the past that was usually enough to win; but not this year.
• And 3 teams submitted 4 correct solutions - that's unheard of. The contestants are getting smarter every year, or we are loosing it.

The postscript version of this article can be found here.

In previous ALP newsletters, readers have read articles that describe several theorem proving systems for higher order logic [4, 2, 5]. This article does the same, but for a higher order logic with a weaker type system than classic higher order logics. The logic in question is referred to as G, which stands for Gilmore; it is inspired by similar logics developed by P. C. Gilmore [3]. Whereas most higher order logics maintain consistency by assigning a type to every term, Gilmore logics maintain consistency by making a distinction between uses and mentions of variables standing for properties. A full description of G can be found in [1].

The phrase ``theorem proving system'' is often used to encompass both fully-automated systems that use AI to prove formulas, and systems that merely help the user to prove a formula. The system described in this paper is definitely in the latter category, a kind of system sometimes referred to as a ``proof assistant''. We therefore call it GPA, for ``G Proof Assistant''.

Formulas and Sequents

Some complex terms also have flavour. A mention term is a term without free use variables. A use term is a term of the form , where is a predicate name or use variable and the s are mention terms. Some terms, like , where and are predicate names and and are mention variables, are both use terms and mention terms. Some terms, like , where is a constant and is a use variable, are neither use terms nor mention terms.

A sequent is an object of the form , where and are multisets of formulas. Usually we write each multiset as a sequence of formulas. A sequent roughly means ``if all of the formulas are true, then at least one of the formulas is true.'' The formulas on the left-hand side of the ``turnstile'' symbol are collectively called the antecedent, and the ones on the right the consequent of the sequent.

Automated theorem provers and proof assistants often use logics based on sequents, because such logics have a pleasantly regular form. A derivation in the logic is a tree of sequents; the leaves are axiom sequents that are true in themselves; the root is the sequent we are trying to prove; and every internal node follows from its children by one of the rules of the logic. Hence, all the rules of the logic consist of zero or more premise sequents and one conclusion sequent. We can prove a formula by proving the sequent , that is the sequent with an empty antecedent and with a consequent consisting only of .

Rules

If the presence of lambda-terms and application and the addition of the above two rules were the only change from first order logic, then the proof system would be inconsistent. The essence of the type-theoretic approach to higher order logic is to add types to all the terms in the rules to ensure consistency. The approach developed by Gilmore uses a much weaker mechanism to ensure consistency.

There are three rules that are different in G than they are in first order logic. The usual first order logic axiom sequent (leaf node) is:

where

where and and are use terms

where is a variable not appearing in , , or

where is a variable not appearing in , , or , and and are the same flavour as

Derivations

We can describe the locations of sequents in the derivation tree. These location descriptors will become important when we talk about GPA. The bottommost sequent is considered to be at location [a]. The children of a sequent at location L are considered to be at locations [a|L], [b|L], and so on. Thus the location descriptors for the above derivation would be:

Recursive Predicates

There is also another way of formulating recursive predicates, which allows us to prove properties involving them more easily. Consider the Peano representation of the natural numbers, in which is a natural number, and for every natural number , is also a natural number (the successor of ). In this representation, 1 is , 2 is , and so on. Let a particular predicate be such that the formula is true, and the formula is true. We can say that is true of 0 and all its successors. If we view as the set of things it is true of, then we can call a zero-successor set. Consider the following term:

Now, we can define the intersection of all sets with a particular property by the following term:

N

GPA also has the notion of a definition of a term, but this is not intended to encompass recursive definitions. We can define term names, say l or n1, as being equivalent to other terms, say the definitions of L and N above. GPA defines ``rules'' for the logic that simply replace a defined term by its definition. We can apply these rules like other rules of G, although strictly speaking this is a metatheoretic facility.

Implementation of GPA

Of course, it would be possible to do so by using what is called a ``term encoding'' of variables - that is, using constants and function symbols to represent variables. But this would be the same as we could achieve in a first order logic. I therefore decided to develop GPA in regular first-order Prolog, since many full-featured interpreters are available for Prolog.

This means, unfortunately for me, that I had to code predicate freevar(M, V) for checking whether variable V appears free in term M, and predicate subst(M, S, T, N) for replacing all free occurrences of S in M everywhere by T, resulting in N. These predicates are much more complex than they would appear at first glance, they must be maintained very precisely whenever the internal representation of terms changes, and if they are wrong, they result in very difficult-to-find bugs.

Using GPA

The intention of the system is like that of every other proof assistant program: we start out with a single ``proof obligation'', the sequent S, and proceed by building a derivation tree. We begin by considering S to be at location [a], and try to run a rule of the logic backward in order to find, for instance, two sequents S1 and S2 that can be premises for that sequent. Those sequents then are placed at locations [2*a] and [b,a] in the partially constructed derivation, and become our new list of proof obligations. In general we have a number of proof obligations, at various locations in the derivation, that can grow as we apply rules and shrink as we arrive at axiom sequents. When our list of proof obligations has shrunk to the empty list, then we have done everything we need to do in order to prove the initial sequent S.

GPA does some of this automatically. GPA will take any steps that it knows will not lead away from a correct derivation. For instance, if it were to arrive at a proof obligation sequent at location L that has a conjunction in the antecedent, GPA would automatically apply the rule for conjunction in the antecedent (see above) and place the premise sequent at location [a|L] in the partially constructed derivation.

However, in building the derivation, GPA will often be stumped about what to do with a particular proof obligation. When it has applied all the rules it can automatically to all the proof obligations it has, it will print out the obligations and their locations and ask the user for a hint.

This is where the ``hints list'' comes in. There is a very primitive sort of interactivity with the theorem prover. The user first poses the query with an empty hints list, and the prover probably asks it for a hint at one or more locations. The user inspects the obligations and figures out what hint might help the system go further. Then the user re-poses the same query, but with the hint added to the hints list. The system (hopefully) is able to go farther, and prints out a new list of unresolvable proof obligations. Eventually there are no unresolvable obligations.

Example

sderiv(
  seqt( ["pdefn"],
        ["forall x . ((n1 x) => (p x))"] ),
  []
).

* Hint needed for sequent at location [3*a]:
  Antecedents:
    1. (n1 x)
    2. pdefn
  Consequents:
    3. (p x)

pdefn(Pdefn), sderiv(
  seqt( ["pdefn"],
        ["forall x . ((n1 x) => (p x))"] ),
  [ h([3*a], def(1)) ]
).

* Hint needed for sequent at location [4*a]:
  Antecedents:
    1. (l \\z. ((z zero) & forall y.
         ((z y) => (z (s y)))) x)
    2. pdefn
  Consequents:
    3. (p x)

* Hint needed for sequent at location [6*a]:
  Antecedents:
    1. forall y. ((\\z. ((z zero) & forall y.
         ((z y) => (z (s y)))) y) => (y x))
    2. pdefn
  Consequents:
    3. (p x)

pdefn(Pdefn), sderiv(
  seqt( ["pdefn"],
        ["forall x . ((n1 x) => (p x))"] ),
  [ h([3*a], def(1)),
    h([4*a], def(1)),
    h([6*a], forall(1,"p"))
  ]
).

* Hint needed for sequent at location [10*a]:
  Antecedents:
    1. pdefn
  Consequents:
    2. (p zero)
    3. (p x)
* Hint needed for sequent at location
    [2*a, b, 9*a]:
  Antecedents:
    1. (p y)
    2. pdefn
  Consequents:
    3. (p (s y))
    4. (p x)

We could now proceed by asking the system to expand the definition of pdefn and using the Horn clauses defined there to prove these two properties of p. Eventually we would get the response

  Sequent derivable.  Derivation:

Conclusions

Bibliography

1

James H. Andrews.
A weakly-typed higher order logic with general lambda terms and Y combinator.
In Proceedings, Works In Progress Track, 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '02), pages 1-11, Hampton Roads, Virginia, August 2002. NASA Conference Publication CP-2002-211736.

2

Amy Felty.
Interactive theorem proving in Twelf.
ALP Newsletter, 15(3), August 2002.

3

Paul C. Gilmore.
NaDSyL and some applications.
In Proceedings of the Kurt Gödel Colloquium, volume 1289 of LNCS, pages 153-166, Vienna, 1997. Springer.

4

Frank Pfenning
Logical frameworks at CMU.
ALP Newsletter, 14(2), May 2001.

5

Brigitte Pientka.
Overcoming performance barriers: Efficient proof search in logical frameworks.
ALP Newsletter, 16(2-3), May-August 2003.

The PDF-version of this article can be found here.

Abstract:

A recent and promising research direction for logic programming is the study of the connections with the techniques used computer aided verification. In the last five years I have studied this problem by focusing on the application of constraint logic programming to the verification of infinite state concurrent systems. This research work started during my postdoctoral visit to the Max Planck Institute for Computer Science in Saarbrücken. Together with Andreas Podelski, we attacked this problem by comparing the semantics of Computational Temporal Logic (CTL) [30,29], a logic at the basis of verification techniques like model checking [20], and the model theoretic semantics of logic programming. As a first observation, we noted that both semantics enjoy a characterization in terms of fixpoint equations. Furthermore, while propositional logic programs can be used to specify finite-state systems, first-order logic programs, and, more in general, constraint logic programs (CLP) could be used to specify infinite-state transition systems (e.g. systems with variables ranging on unbounded integers). The previously described connection suggested us that the fixpoint semantics of constraint logic programs could be used as a procedure for automated verification of infinite-state systems [15]. Based on these ideas, we built the prototype DMC for model checking infinite-state systems using Constraint Logic Programming described in [16]. Constraints were used here to finitely represent infinite sets of states. Different constraint solvers (e.g. a constraint solver for reals, and a constraint solver for boolean formulas) were used to efficiently handle this representation within the fixpoint computation used to check safety and liveness properties of infinite-state transition systems specified as CLP programs. We applied successfully our prototype to automatically verify safety and liveness properties for skeletons of communication protocols (with a fixed number of processes) like the well-known bakery and ticket mutual-exclusion algorithms. In these case-studies the source of infiniteness was due to the presence of potentially unbounded integer variables in the specification of individual processes (i.e. the tickets used by process to enter the critical section). Our verification procedure was built on a constraint solver for real arithmetics. In [16], however, we have shown that the relaxation integer-reals (a technique peculiar of integer linear programming) does not lose precisions when applied to protocols like those verified in [15] where constraints modeling guards and updates are conjunctions of formulas of the form x - y c where x and y are variables and c is a constant.

Differently from previous work done in the area of verification and logic programming like [25,27,31], our approach was the first proposing a connection between CTL properties (and not only safety properties as in [25,27]) of discrete concurrent systems and the fixpoint semantics of CLP programs.

The next challenge for our constraint-based approach to verification was to find new case-studies. Parameterized verification turned out to be an ideal setting for our technology.

Concurrent systems consisting of a finite, but a priori unknown number of identical, finite-state components is one of the more interesting example of infinite-state system. They occur in several different contexts like protocols for multiprocessor systems, client-server architectures, distributed databases, and web-based applications. The challenge here is to find automatic techniques to formally verify, e.g., safety properties, for configurations in which the number of components is left as a parameter (see e.g. [2,21,23,22,26]). Broadcast protocols, introduced by Emerson and Namjoshi in [22], represent one example of this kind of concurrent systems. In a Broadcast protocol processes are allowed to communicate via rendez-vous (one-to-one communication) as well as via broadcast messages (one-to-many communication). In collaboration with Javier Esparza and Andreas Podelski, in [13], we shown that constraint-based technology could be naturally applied to verify these systems. The idea here was to apply what we called counting abstraction, i.e., use integer variables to count the number of processes in a given state during the execution of a protocol. In [13], we shown that special classes of integer linear constraints could be used as symbolic representation of the global state of a Broadcast protocol (global state = collection of local states at a given instant during the protocol execution). This result implies that constraint-based tools like the one we built in [16] can be applied to automatically verify properties of this class of infinite-state systems. The strategy used in [13] is symbolic backward reachability: starting from the set of unsafe state (expressed via constraints), one tries to show that the initial state is not contained into the saturated set of predecessor states, represented symbolically via disjunctions of constraints. (This kind of analysis also corresponds to a bottom-up evaluation of a CLP program describing the transitions of a Broadcast protocol, see [16]). The termination of the analysis is guaranteed by the well-quasi ordering of the entailment relation defined over the constraints considered in [13]. The results in [13] are an instance of the general decidability results for infinite-state model based on well-quasi orderings given in [1,24].

Based on the preliminary ideas in [13], we found a very interesting application of constraint-based technology for the verification of the correct design of cache coherence protocols [7]. Cache coherence protocols are used in multiprocessor systems with shared memory in order to ensure the consistency of data in presence of local caches [28]. At an adequate level of abstraction, these protocols can be modeled using an extension of Broadcast protocols in which, apart from rendez-vous and broadcast communication (used to model notification signals), global conditions (e.g. if all caches are invalid then ...) are used as guards for protocol transitions [7]. Though global conditions break decidability for verification of safety properties (they introduce zero-tests in the abstract model with counters), constraint-based tools can still be applied as `incomplete' verification methods. In the experiments performed in [7] using the constraint-based model checker described in [16], we managed to verify the correctness of a large number of coherence protocols taken from the literature. It is important to note that, thanks to the counting abstraction mentioned in the previous section, the verification was carried out for any possible system configuration, i.e. any number of processors.

In [8], we have applied this technique to verify properties of the Futurebus cache coherence protocol, a protocol that, due to the complexity of its functionalities, deserves special attention.

Finally, in collaboration with Tevfik Bultan (University of California at Santa Barbara) in [12] we have applied similar techniques to verify client-server protocols, like home-based consistency protocols, i.e. protocols designed for systems with a central monitor that serializes the accesses to shared data. For this class of protocols, it is convenient to consider abstract models built via counters and global Boolean variables used as guards in the corresponding transitions. In order to symbolically handle global states for this kind of models, we used a combination of Presburger and Boolean constraints incorporated in the backward reachability strategy described above. Symbolic backward reachability can be applied to Broadcast protocols as well as to Petri Nets to solve safety properties and coverability problems [1,24]. Unfortunately, in [13] we have experimentally verified that constraint-based verification tools built on standard constraint solver for linear arithmetics (e.g. using simplex or Fourier-Motzkin methods) may suffer from the ``symbolic state explosion problem'' when applied to large Petri nets. The problem consists in the explosion of the number of constraints (i.e. the size of the disjunctions) generated during backward search. To alleviate this problem, in collaboration with Jean-Francois Raskin (Universitè Libre de Bruxelles and formerly a member of the Max Planck Institute) We have started working on efficient representations of large collections (disjunctions) of linear constraints. In [17], we have adopted a data structure called Covering Sharing Trees (CSTs) in order to compactly represent collections of constraints representing upward closed sets of tuples of integer numbers (hence Petri Net markings), or equivalently disjunctions of linear constraints having the the form x₁ c₁,...x_n c_n where c_i is a non-negative integer (e.g. 3 x₂ 10...). CSTs are acyclic graphs used to store the constants in the previous kind of constraints (e.g. 3, 10,... is a path in the corresponding CST), and in which we allow the maximum sharing of its prefixes and suffixes.
In [17], we have defined all operations needed to lift backward reachability to a CST-based symbolic representation. Unfortunately, some of these operations have exponential cost (e.g. checking subsumption between two disjunctions of constraints represented as CSTs is co-NP hard in the size of the graphs). To overcome this obstacle, we have found sufficient conditions based on simulation relations between nodes of CSTs that can be used to check subsumption and eliminate redundant constraints efficiently. These heuristics seems to work well in practice. In [18], we have further improved our methods by using invariants computed statically via the structural theory of Petri Nets [32]. The idea here is to cut the backward search space by taking into account information coming from the initial states like Place invariants. Place invariants return information like the number of tokens in place p₁ and p₂ will be always equal to 1, thus restricting the set of markings one needs to explore. Place invariants can be computed by applying linear programming techniques before starting to explore the state space of a Petri Net [33]. The results are very promising as shown by the several experiments discussed in our work [18]. We are currently working on the extension of this technique in order to be able to analyze not only Petri Nets but also extensions of them like Broadcast protocols [19].

Following this line of thoughts, in collaboration with Marco Bozzano we have extended the fixpoint semantics (bottom-up evaluation) to first-order LO programs, or, better, LO programs annotated with constraints (i.e. the lifting of CLP to linear logic programs with multi-headed clauses). Though termination can be guaranteed only for special fragments [4], we were able to define an effective fixpoint operator à-la T_P (the immediate consequence operator for (constraint) logic programs). This operator can be viewed as a symbolic predecessor operator for transition systems described via multiset rewriting systems defined over first-order atomic formulas (as in the MSR formalism introduced by Cervesato et al. [6]). As main case-study, we recently manage to automatically verify (as far as we know for the first time) mutual exclusion for a parameterized formulation of the ticket mutual exclusion protocol [4]. As sketched in [9], these ideas represent a first step towards the analysis of systems parametric in several dimensions, i.e., parametric in the number of processes (as in Petri Nets and Broadcast protocols) as well as in the value of data attached to each processes (transitions are describe, in fact, via first order atoms). Furthermore, in [3] we have extended the formalisms of MSR with constraints with a global synchronization mechanism so as to specify and verify properties of invalidation protocols. The resulting verification framework can be used in several different applications like the analysis of mobile processes [11] and the verification of secrecy and authentication properties for cryptographic protocols [14] (a joint work with Pierre Ganty of the Universitè Libre de Bruxelles).

In this paper we have described some techniques based on extensions of (Constraint) Logic Programming that can be used for the verification of infinite-state systems. Finding scalable in practice methodology for the application of these techniques to the verification of (abstract models of) concurrent software is probably the more intriguing future research direction for our work. Further research on efficient data structures and abstraction techniques seems necessary however for pursuing such a difficult and challenging goal.

1

P. A. Abdulla, K. Cerans, B. Jonsson and Y.-K. Tsay.
General Decidability Theorems for Infinite-State Systems.
LICS 1996: 313-321.

2

P. A. Abdulla and B. Jonsson.
Verifying Networks of Timed Processes.
TACAS 1998: 298-312.

3

M. Bozzano and G. Delzanno
Algorithmic Verification of Invalidation-based Protocols
CAV 2002: 295-308.

4

M. Bozzano and G. Delzanno.
Beyond Parameterized Verification.
TACAS 2002: 221-235.

5

T. Bultan, R. Gerber, and W. Pugh.
Symbolic Model Checking of Infinite-state Systems using Presburger Arithmetics.
CAV 1997: 400-411.

6

I. Cervesato, N. A. Durgin, P. Lincoln, J. C. Mitchell and A. Scedrov.
A meta-notation for protocol analysis.
CSFW 1999: 55-69.

7

G. Delzanno.
Automatic Verification of Parameterized Cache Coherence Protocols.
CAV 2000: 53-68.

8

G. Delzanno.
Verification of Consistency Protocols via Infinite-state Symbolic Model Checking, a Case Study.
In FORTE/PSTV 2000: 171-188.

9

G. Delzanno.
An assertional language for systems parametric in several dimensions (Preliminary results).
ENTCS 50: 373-387, 2001.

10

G. Delzanno.
Constraint-based Verification of Parameterized Synchronous Systems.
FroCos 2002: 72-86.

11

G. Delzanno
A Symbolic Procedure for Control Reachability in the Asynchronous Pi-calculus
Infinity'03, a Satellite workshop of Concur 03, September 2003.

12

G. Delzanno and T. Bultan.
Constraint-based Verification of Client-server Protocols.
CP 2001: 286-301.

13

G. Delzanno, J. Esparza, and A. Podelski.
Constraint-based Analysis of Broadcast Protocols.
CSL 1999: 50-66.

14

G. Delzanno and P. Ganty
Automatic Verification of Time-sensitive Cryptographic Protocols
TACAS 2004: 342-356.

15

G. Delzanno, and A. Podelski.
Model Checking in CLP.
In TACAS 1999:223-239.
The authors received the award for the best paper of ETAPS '99 assigned from the European Association for Programming Languages and Systems.

16

G.Delzanno and A. Podelski.
Constraint-based Deductive Model Checking.
STTT 3(3): 250-270, 2001.

17

G. Delzanno, and J. F. Raskin.
Symbolic Representation of Upward-closed Sets.
TACAS 2000: 426-440.

18

G. Delzanno, J.-F. Raskin, and L. Van Begin.
Attacking Symbolic State Explosion.
CAV 2001: 298-310.

19

G. Delzanno, J.-F. Raskin, and L. Van Begin.
Towards the Automated Verification of Multithreaded Java Programs.
TACAS 2002: 173-187.

20

E. M. Clarke and E. A. Emerson.
Synthesis of synchronization skeletons for branching time temporal logic.
In Logic of Programs, LNCS 131, Springer-Verlag. 1981.

21

E. Clarke, O. Grumberg, S. Jha.
Verifying Parameterized Networks.
TOPLAS 19(5): 726-750 (1997).

22

E. A. Emerson and K. S. Namjoshi.
On Model Checking for Non-deterministic Infinite-state Systems.
LICS 1998: 70-80.

23

J. Esparza, A. Finkel, and R. Mayr.
On the Verification of Broadcast Protocols.
LICS 1999: 352-359.

24

A. Finkel and P. Schnoebelen.
Well-structured transition systems everywhere!
TCS, 256: 63-92, 2001.

25

L. Fribourg and J. Richardson.
Symbolic Verification with Gap-order Constraints.
Technical Report LIENS-93-3, Laboratoire d'Informatique, Ecole Normale Superieure, Paris, 1996.

26

S. M. German, A. P. Sistla.
Reasoning about Systems with Many Processes.
JACM 39(3): 675-735 (1992)

27

G. Gupta and E. Pontelli.
A Constraint Based Approach for Specification and Verification of Real-time Systems.
RTSS'97.

28

J. Handy.
The Cache Memory Book.
Academic Press, 1993.

29

Z. Manna and A. Pnueli.
Temporal Verification of Reactive Systems: Safety.
Springer-Verlag, 1995.

30

A. Pnueli.
A temporal logic of concurrent programs.
TCS 13:45-60, 1981.

31

Y. S. Ramakrishnan, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren.
Efficient Model Checking using Tabled Resolution.
CAV 1997:143-154.

32

W. Reisig.
Petri Nets. An introduction. EATCS Monographs on Theoretical Computer Science, Springer 1986.

33

M. Silva, E. Teruel, and J. M. Colom.
Linear Algebraic and Linear Programming Techniques for Analysis of Place/Transition Net Systems.
Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, LNCS 1491:308-309, 1998.

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.70)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -verbosity 3 -split 0 -no_navigation -antialias -antialias_text -html_version 4.0,math delzanno.tex

The translation was initiated by Enrico Pontelli on 2004-05-03

ECLiPSe 5.7 was released at the end of last year, and is the current stable and recommended release of ECLiPSe.  The highlights in this release are the port to Apple's MacOS X operating system, several new visualisation features, new code analysis tools, and a new version of the ic interval solver.  The next major release is now planned for the autumn of 2004.

More details are available from the ECLiPSe Web Site at IC-Parc, Imperial College London.

General Overview of ECLiPSe

ECLiPSe is a software system - based on the CLP paradigm - for the development and deployment of constraint programming applications. It is also ideal for teaching most aspects of combinatorial problem solving, e.g. problem modelling, constraint programming, mathematical programming, and search techniques. Its wide scope makes it a good tool for research into hybrid problem solving methods. A growing number of universities use ECLiPSe for teaching, and it is referred to in the main CLP textbooks. ECLiPSe comprises several constraint solver libraries, a high-level modelling and control language, interfaces to third-party solvers, an integrated development environment and interfaces for embedding into host environment

The ECLiPSe programming language is largely backward-compatible with Prolog and supports different dialects. It provides however an extended set of basic data types (byte strings, unlimited precision integer and rational numbers, double precision floats and double precision intervals). Syntax extensions like array syntax and structures with field names are supported and are especially useful in constraint modelling. A logical iteration construct eliminates the need for most simple recursion patterns. Comprehensive facilities to implement data-driven control behaviour are available. These include declarative delay-clauses as well as primitives for meta-programmed control like explicit goal suspension, flexible triggering facilities and execution priorities. The attributed variable data type is the key to many extensions to the basic Logic Programming language. The module system controls the visibility of predicates, non-logical stores, source transformations and syntax settings. Module interfaces can be extended and restricted, and modules written in different language dialects can be mixed within one application. Programs may contain structured comments from which reference documentation can be generated.

ECLiPSe provides several libraries of constraint solvers which can be used in application programs: Arithmetic constraints over finite domains, finite set constraints, generalized propagation (Propia), interval reasoning over non-linear constraints, interfaces to external simplex solvers, constraint handling rules (CHR) and more. Other libraries implement search methods like branch-and-bound, repair-based search, limited discrepancy search and others.

ECLiPSe integrates to external solvers. In particular, the academic distribution of ECLiPSe comes bindled with a full version of XPRESS-MP, one of the leading commercial linear and mixed-integer programming solvers. By kind agreement of Dash Optimization, the academic use of this solver via the ECLiPSe eplex-interface is covered by the standard ECLiPSe license agreement, opening up new opportunities for research on large-scale real-life problems.

TkEclipse Aqua Look

Easier Installation

Good news for Windows and Linux users: as an alternative to the classical distribution in the form of compressed tar (tgz) files, there are now dedicated installer packages for these two operating systems. The Windows version can be downloaded as a single installer file (e.g. ECLiPSe5.7_31.exe) and installed by executing this file and going through a straightforward installation dialog. For Linux, we have made rpm-packages available, which should make system-wide installations and version control simpler for the Linux system administrator.

Visualisation Features

The development system's visualisation client has been extended with a whole range of new viewers. This means that you can now visualise your collections of program variables as Fixed Network, 0/1 Network, Capacity Network, Gantt Chart or Bar Chart, in addition to the previously existing Text table, Bounds table, Fade table and Desktop layout views. Another interesting new feature is the possibility to visualise variable attributes like tentative values and eplex solutions.

Visualisation Client with Gantt and Bar Charts

The new graph drawing facilities used in the network viewers are in fact built on top of AT&T's Graphviz tools. We have included these tools with this ECLiPSe distribution, so you don't need to download anything separately. Also, you can easily access these graph drawing tools directly from your ECLiPSe program using the new lightweight lib(graphviz) interface library.

Another nice application of graph drawing is the cross-referencing tool lib(xref). To see what it can do, simply select Cross Referencer from TkEclipse's File menu and apply it to one of your ECLiPSe source files!

The call graph of an ECLiPSe program

Performance analysis is an important problem in particular in Constraint Programming, because, owing to the complex interaction of algorithms and control parameters, it is often not easy for the programmer to identify resource (time or memory) bottlenecks in a program. As art of our ongoing efforts to produce tools to assist with this task, this release contains the instprofile library, which provides two complementary mechanisms for the profiling of ECLiPSe code with any of the metrics provided by the statistics/2 predicate.

The first one is instrumentation based, where metric measuring code is inserted directly into the user program in order to accurately determine how its constituent pieces of code perform. The mechanism for the insertion of instrumentation code is based upon the facilities of the instrument library. As such, the statistic measurements may be inserted at the beginning and end of clause or block definitions, and around subgoals and/or predicate calls.

The second alternative is sample driven, where metric measuring code is executed at a user defined interval as the user program runs. The sample based profiler is implemented using after events and is therefore less intrusive in its effect on the performance of the executing code.

This release contains a revised version of the lib(ic) interval solver, giving better performance and rectifying some cases of previously unclear semantics.

If you are using lib(fd) and have not been using lib(ic) so far, then this is the time to switch! The lib(ic) library is a general interval propagation solver which can be used to solve problems over both integer and real variables. Integer variables behave much like those in lib(fd), while real variables behave much like those from the old real interval arithmetic solver lib(ria).

IC allows both kinds of variables to be mixed seamlessly in constraints, since (with a few exceptions) the same propagation algorithms are used throughout and all variables have the same underlying representation (indeed, a real variable can be turned into an integer variable simply by imposing an integrality constraint on it).

The PDF-version of this article can be found here.

A Brief History

On December 9, 1998 we e-mailed the following message to several students and friends:

  Subject: Would you like to join TAG?

                     Texas Action Group:
           The University of Texas Research Group
          for the Study of Reasoning about Actions

  Texas Action Group (TAG) is a newly organized group of
  researchers interested in the study of formal and automated
  reasoning about the effects of actions using action
  languages, logic programming under the answer set semantics,
  and related ideas.  It is led by Michael Gelfond (University
  of Texas at El Paso) and Vladimir Lifschitz (University of
  Texas at Austin).  TAG members will use a mailing list and a
  web page to communicate on topics of common interest.

  Although TAG is being created primarily for the benefit of
  graduate students and faculty of the University of Texas,
  membership is open to anyone.

  If you would like to join TAG, please send a request to
  Vladimir Lifschitz (vl@cs.utexas.edu).  Then your name and
  e-mail address will be placed on the TAG home page; we will
  also provide a link to your personal page if your message
  includes the URL.

  Please forward this announcement to your colleagues who you
  think may be willing to participate.

Today, more than five years later, this ``Texas group'' includes many participants from other parts of the United States and from other countries, including Austria, Canada, China, Germany, Italy, Mexico, Spain and Turkey. The topics we are discussing now include many subjects other than reasoning about actions, but one thing has not changed: our interests are centered around the use of logic programs as a knowledge representation tool. Many of our technical discussions are related to answer set programming.

For the most part, TAG members communicate with each other electronically, but we do meet and talk face to face once in a while. More than 30 TAG members met last August at a meeting organized in New Mexico by Enrico Pontelli and Tran Cao Son. More than 20 participants of LPNMR-7 took part in a traditional TAG lunch in Fort Lauderdale in January of 2004.

To learn more about TAG, check our home page

Texas Action Group at Austin

Vladimir's ``TAG team'' includes four doctoral students this year: Selim Erdogan, Paolo Ferraris, Joohyung Lee and Wanwan Ren. Here are some of the research topics that we in Austin are interested in.

Applications of logic programming to historical linguistics.

The evolutionary history of families of natural languages, such as the Indo-European family, can be described in terms of ``temporal phylogenetic networks.'' These networks contain information about genetic relationships between linguistic communities and about interactions between them, including chronological information. The discrete data from a network can be conveniently represented in answer set programming languages; for the chronological part, constraint programming languages are more appropriate. In our experiments, the ASP system CMODELS and the CP system ECLIPSE work together to solve computational problems from historical linguistics.

Why is exchanging hats irrelevant?

In one of the enhancements of the Missionaries and Cannibals problem introduced by John McCarthy, missionaries have hats, and they can exchange them, if they wish. This action is irrelevant, of course, if the goal is to cross the river. We are looking at the ``missionaries with hats'' domain represented in action language C+, closely related to logic programming, and we'd like to identify the syntactic features of this domain that make the action of exchanging hats irrelevant.

General purpose database of properties of actions.

Commonsense reasoning domains involving actions, such as the blocks world and the Missionaries and Cannibals domain, have many common features. For instance, they often involve physical objects that change their positions in space. We would like to isolate the concepts and principles that these domains have in common and to compile a database of such principles, stated in a general form, and expressed in action language C+.

Semantics of aggregates in ASP languages.

Cardinality and weight constraints in the language of lparse are the best known examples of aggregate constructs in the input languages of answer set solvers. Such constructs are used routinely in applications of ASP. Several definitions of the semantics of aggregates described in the literature are not always equivalent to each other, and in some cases their properties seem unintuitive. We'd like to clarify the relationship between various versions of the semantics of aggregates, and to find the ``right'' definition.

Efficient elimination of weight constraints.

Weight constraints can be eliminated from a logic program in favor of additional atoms. The answer set solver cmodels uses this fact to reduce the problem of computing answer sets for programs with weight constraints to SAT. In the special case of cardinality constraints, the elimination process is efficient, in the sense that it does not lead to a significant increase in the size of the program. But in the general case the increase in size can be exponential. We are working on a translation that is efficient for arbitrary weight constraints.

Relationship between modular translations and strong equivalence.

We are interested in general properties of the translations that do not introduce additional atoms, but rather turn a logic program into an equivalent program-a program with exactly the same answer sets. For instance, there exists a modular (rule-by-rule) transformation that turns any program with weight constraints into a program with nested expressions. Another example of a modular equivalent transformation is given by the process of converting programs with monotone cardinality atoms into programs with cardinality constraints. There seems to be a close relationship between modular equivalent transformations and the concept of strong equivalence. We would like to make this idea precise.

Loop formulas.

The invention of loop formulas by Fangzhen Lin and Yuting Zhao was perhaps the most significant event in the area of LPNMR in recent years. The related work to which members of the Austin team have contributed is described in the papers ``Loop formulas in disjunctive logic programs'' (Proc. ICLP'03), ``Nondefinite vs definite causal theories'' (Proc. LPNMR-7), ``Loop formulas for circumscription'' (to appear in Proc. AAAI'04), and ``Why are there so many loop formulas?'' (to appear in ACM Transactions on Computational Logic). We plan to further explore this intriguing idea and its potential applications.

More information about the Austin group can be found at its web page:

• ICLP'03 Proceedings on Sale
• INTAS Thematic and Collaborative Calls
• WIN-PROLOG in the News
• Release of PRISM 1.7

The ICLP 2003 and ASIAN 2003 proceedings are on sale at a subsidized rates:

• 19th International Conference, ICLP 2003 Proceedings LNCS 2916: USD 25.00
• Advances in Computing Science - ASIAN 2003 LNCS 2896: USD 20.00.

• INTAS Thematic Call for Proposals for Research Projects and Networks on Information Technology (indicative budget Euro 1 million)
• INTAS Thematic Call for Proposals for Research Projects and Networks on Position Sensitive Detectors (indicative budget Euro 800,000)
• INTAS Thematic Call for Proposals for Research Projects and Networks on Transforming Societies: East and West (indicative budget Euro 1.5 million)
• INTAS Collaborative Call with Airbus for Proposals for Research Projects in the field of Aeronautics (indicative budget Euro 1 million)
• INTAS Collaborative Call with Kazakhstan for Proposals for Research Projects on Management of Man-made Pollution (indicative budget Euro 1.5 million)
• INTAS Collaborative Call with Uzbekistan for Proposals for Research Projects on Sustainable Development through the Use of Local Natural Resources and New Technologies (indicative budget Euro 1 million)

Read an interesting article from the NY Times: http://www.nytimes.com/2004/03/13/arts/13BOOK.html?ex=1079758800&en=cd8e454dc3dee2a5&ei=5062&partner=GOOGLE. Inflow is written in LPA Prolog for Windows. For more on InFlow visit: http://www.orgnet.com.

PRISM is a logic-based probabilistic language and is easy to learn and use for anyone who is familiar with Prolog.
PRISM is suitable for modeling those statistical phenomena that are governed by rules and probabilities such as statistical natural language processing, game analysis, data mining, performance tuning, and bio-sequence analysis. PRISM has the following unique features:

1. The user can use programs to define distributions over terms and atoms.
   Mathematically a PRISM program is a formal object which defines a probability measure over the set of possible Herbrand interpretations. The distributions are derived and computed from the defined measure. There are no restrictions on programs, e.g., programs are not required to be range-restricted or Datalog programs.
   
   
2. Parameters in a program are learnable automatically from examples.
   A PRISM program contains statistical parameters that reflect the statistical properties of the model. They can be automatically estimated from examples by ML (Maximum Likelihood) estimation performed by a built-in EM learning routine.
   
   
3. Probabilities are computed efficiently in a dynamic programming manner.
   PRISM uses "explanation graphs" to compute probabilities and learn parameters, where solutions are shared as in dynamic programming. Explanation graphs are constructed by tabled search.
   
   
4. PRISM is a high level yet efficient modeling language.
   Popular symbolic-statistical models such as hidden Markov models, probabilistic context free grammars and Bayesian nets can be described in PRISM in a very compact way. Their parameter learning in PRISM can be done as efficiently as those by specialized EM algorithms such as the Baum-Welch algorithm. In addition, PRISM can be used to model certain phenomena that are hard to model using the specialized statistical tools.

PRISM1.7 is the latest version of PRISM, which is implemented on top of B-Prolog and makes use of B-Prolog's efficient linear tabling mechanism for tabled search. This version is considerably more efficient in both time and space than the previous version, PRISM1.6, thanks to improved tabled search. It also provides new built-ins that facilitate modeling and learning. PRISM1.7 is sustainable to relatively large sets of data and would be of interest to anyone who would like to challenge statistical modeling of complex phenomena.

• Do My Homework and Mainstreaming Prolog
• N-Solutions in Mercury and Declarativity

E.g., remove_largest([1,3,5,9,7,4,5],X)? %largest item is 9
X=[1,3,5,7,4,5]

:remove_largest([1,9,5,9,7,4,5],X)? %largest item is 9 in position 2
X=[1,5,9,7,4,5] % note that the second occurence of the largest number
remains.

You need to use something like this :

    remove_nine([9|T], T).

You need to write a predicate that searches through the whole list, and when it finds a nine, it removes it using something like the line above.
I won't tell you the whole answer, because you are learning prolog, and it will be good for you to solve the rest of it yourself.

Quoting Martin Sondergaard in comp.lang.prolog:
> I won't tell you the whole answer, because you are learning prolog,
> and it will be good for you to solve the rest of it yourself.
>

Which is better:

• to get quick help to get over and understand the basics in order to get to like the language and find the interest needed to move on and develop ones Prolog skills, or
• to spend hours, days or even weeks with not getting anywhere far and develop total dislike of the Prolog language and it's seemingly closed Community and leave quickly as soon as the course is done with (presumably with the help of last minute cheating just to get rid of it)?

I don't understand your point. Are you saying that it is better both for the individual and for the Prolog community to do this individual's homework from A to Z instead giving him a hint?...

Quoting Andrzej Lewandowski in comp.lang.prolog:
> I don't understand your point. Are you saying that it is better both
> for the individual and for the Prolog community to do this
> individual's homework from A to Z instead giving him a hint?...

My point is really a general one.

I am saying that in general there is very little Prolog entry level help to find compared with for instance Java and C/C++.

You can find numerous implementations of almost any algorithm or even smaller programs in the latter languages, wheras in Prolog it seems all you get is "invent the wheel again". Implied is "we learnt the hard way, so shall you".

Perhaps I am being too harsh on the Prolog Community, but my feeling is that it is a relatively closed one, in general.

My main question still stands: Is there really a desire within the Prolog Community to increase Prolog's popularity and usage?

> Quoting Andrzej Lewandowski in comp.lang.prolog:
>
>> I don't understand your point. Are you saying that it is better both
>> for the individual and for the Prolog community to do this
>> individual's homework from A to Z instead giving him a hint?...
>
> My point is really a general one.
>
> I am saying that in general there is very little Prolog entry level help to
> find compared with for instance Java and C/C++.
>
> You can find numerous implementations of almost any algorithm or even
> smaller programs in the latter languages, wheras in Prolog it seems all you
> get is "invent the wheel again". Implied is "we learnt the hard way, so
> shall you".

There are enough educational materials, both printed and on-line. Majority of Prolog books are still in print and can be purchased. There are books available on-line. Vendors have on-line tutorials. Google works perfectly if you want to find sample Prolog programs. Agree, not that many books are about Prolog as about Java and not that many Prolog materials exist as C# materials. However, taking into account the size of "Prolog niche", the amount of materials is quite substantial. The only problem, you have to invest some energy if you want to find these materials.

If somebody asks such questions as: "where I can find a tutorial", "what is the best book", "why my program doesn't work", then he/she gets immediate answer and sometimes question triggers long discussion. However, this is somehow a tradition of "Prolog community" not to answer such questions as "how to do my homework". In other words, if you want to get intelligent answer, you must ask intelligent question. "Prolog community" is not different in this respect than "C++ community" or "Java community". Check how "C++ community" reacts to "do my homework" question.

> Perhaps I am being too harsh on the Prolog Community, but my feeling is
> that it is a relatively closed one, in general.
>
> My main question still stands:
>
> Is there really a desire within the Prolog Community to increase Prolog's
> popularity and usage?

Yes, but not by doing somebody's homework.

Quoting Andrzej Lewandowski in comp.lang.prolog:
> There are enough educational materials, both printed and on-line.
> Majority of Prolog books are still in print and can be purchased.
> There are books available on-line. Vendors have on-line tutorials.
> Google works perfectly if you want to find sample Prolog programs.
> Agree, not that many books are about Prolog as about Java and not
> that many Prolog materials exist as C# materials. However, taking
> into account the size of "Prolog niche", the amount of materials is
> quite substantial. The only problem, you have to invest some energy
> if you want to find these materials.

I can't see that there is enough. Not enough as in as in clear descriptions of a broad set of general algorithms and useful little programs that really describes the workings. All books and all sites take you just so long and not any longer.

> If somebody asks such questions as: "where I can find a tutorial",
> "what is the best book", "why my program doesn't work", then he/she
> gets immediate answer and sometimes question triggers long
> discussion. However, this is somehow a tradition of "Prolog
> community" not to answer such questions as "how to do my homework".
> In other words, if you want to get intelligent answer, you must ask
> intelligent question. "Prolog community" is not different in this
> respect than "C++ community" or "Java community". Check how "C++
> community" reacts to "do my homework" question.

The problem is that many of us who "must" learn Prolog will have only a few weeks to learn (and learn to like!) a completely new language (and most often a completely new paradigm). We encounter the language in a more or less compulsory course (often also including entry level theoretical AI which consumes education time!) in parallel with other tight courses.

We just don't have the time to invent the wheel again, to fiddle around and play with Prolog. Like it or not but Prolog is to many of us an anomaly in the education path, or becomes, because of the real (or perceived) high threshold. We just don't see what the payback will be from whatever time we allocate to try to learn the language during those few weeks.

>Yes, but not by doing somebody's homework.

I hope you understand at least in part where I'm coming from here.

Put another way:

Why don't the Prolog people/AI people (often the same, no?) use the 6-7 weeks they have with thousands and thousands of students to buy them over to their paradigm by helping them over that threshold? That would enable more of the students to drive deeper into Prolog and possibly finish the course with a desire to take that vital "2nd course".

Again (yeah I'm today's parrot... :-) ): Is there really a desire within the Prolog Community to increase Prolog's popularity and usage?

On Sat, 13 Mar 2004 20:17:45 +0100, anders t wrote:
> Quoting Andrzej Lewandowski in comp.lang.prolog:
>
>> There are enough educational materials, both printed and on-line.
>> Majority of Prolog books are still in print and can be purchased.
[...]
>> if you want to find these materials.
>
> I can't see that there is enough. Not enough as in as in clear descriptions
> of a broad set of general algorithms and useful little programs that really
> describes the workings. All books and all sites take you just so long and
> not any longer.
>

I don't buy the argument. Examples:

Ivan Bratko, Prolog Programming for Artificial Intelligence. Over 100 programs available from book web site, starting from sorting, searching, trees and such, ending with some quite advanced problems as expert systems, machine learning and inductive programming,

T. van Le, Techniques of Prolog Programming with Implementation of Logical Negation and Quantified Goals. Same as above - a lot of programs covering basic algorithms and advanced topics - expert ssystems, simulation, natural language. Programs not available on line but on attached diskette,

Michael Covington and others, Prolog programming in Depth. As above, over 100 programs from basics to advanced. All programs available on author's FTP server.

In addition, last 2 books are good for people doing "paradigm shift" - there is a comparison of "conventional" (i.e. procedural) and logical approach.

There is also older book, Helder Coehlo, Jose C. Cotta, Prolog by Example: How to Learn Teach and Use it. Available only in libraries this book has ONLY examples - sample problems with solutions. Over 400 pages of sample programs.

Finally, web sites, such as the following:

"P-99: Ninety-Nine Prolog Problems... The purpose of this problem collection is to give you the opportunity to practice your skills in logic programming. [...] The problems have different levels of difficulty. Those marked with a single asterisk (*) are easy. If you have successfully solved the preceeding problems you should be able to solve them within a few (say 15) minutes. Problems marked with two asterisks (**) are of intermediate difficulty. If you are a skilled Prolog programmer it shouldn't take you more than 30-60 minutes to solve them. Problems marked with three asterisks (***) are more difficult. You may need more time (i.e. a few hours) to find a good solution..." Do you need more?

> The problem is that many of us who "must" learn Prolog will have only a few
> weeks to learn (and learn to like!) a completely new language (and most
> often a completely new paradigm). We encounter the language in a more or
> less compulsory course (often also including entry level theoretical AI
> which consumes education time!) in parallel with other tight courses.

You "must" learn calculus, circuit theory, computational complexity. Do you complain about these topics as you complain about Prolog?...

> We just don't have the time to invent the wheel again, to fiddle around and
> play with Prolog. Like it or not but Prolog is to many of us an anomaly in
> the education path, or becomes, because of the real (or perceived) high
> threshold. We just don't see what the payback will be from whatever time we
> allocate to try to learn the language during those few weeks.

Do you have any "payback" for whatever time you allocate to learn calculus or linear algebra?...

> Put another way: > > Why don't the Prolog people/AI people (often the same, no?) use the 6-7
> weeks they have with thousands and thousands of students to buy them over
> to their paradigm by helping them over that threshold? That would enable
> more of the students to drive deeper into Prolog and possibly finish the
> course with a desire to take that vital "2nd course".

Consider my posting a "help". What other "help" you are expecting?...

> Again (yeah I'm today's parrot... :-) ): Is there really a desire within
> the Prolog Community to increase Prolog's popularity and usage?

What is "Prolog community"?... What regards me, I consider myself a member of "Prolog community" to the same extent as a member of "Black&Decker electric drill community". I am using Prolog as a tool and electric drill as a tool. I really don't care whether they are popular or not. And I don' develop emotional attachment towards tools.

Andrzej Lewandowski wrote:
> On Sat, 13 Mar 2004 20:17:45 +0100, anders t wrote:
>
>> The problem is that many of us who "must" learn Prolog will have only a few
>> weeks to learn (and learn to like!) a completely new language (and most
>> often a completely new paradigm). We encounter the language in a more or
>> less compulsory course (often also including entry level theoretical AI
>> which consumes education time!) in parallel with other tight courses.
>>
> You "must" learn calculus, circuit theory, computational complexity.
> Do you complain about these topics as you complain about Prolog?...

This is not a very good argument. I think it is a valid argument to state that a proffesional computer scientist should be familiar with all major paradigms and not with the few that happen to be the most popular in the commercial world today. Being proffesional means you can reason about what you are doing and that requires a broader view. Each day I'm programming (quite often :-) it helps me to think about the problem at hand in the most suitable paradigm, even if other requirements force me to implement it in a less suitable paradigm. Likewise it is useful to know about logic, even though you can not/hardly use it for programming.

I think that problem is that students don't want to study any more, they just want quickly acquire skills that they can sell immediately on the job marked.

Tell me what's wrong with that...?

Perhaps you really wanted to say something else, Andrzej?

anders t wrote:
> Quoting Andrzej Lewandowski in comp.lang.prolog:
>
>> I think that problem is that students don't want to study any more,
>> they just want quickly acquire skills that they can sell immediately
>> on the job marked.
>
> Tell me what's wrong with that...?
> Perhaps you really wanted to say something else, Andrzej?

This is exactly what I wanted to say. Some students don't see the difference between the university and vocational school.

Forgive me but your interpretation of what you said does not match with mine. In my interpretation you said that "it is wrong to aquire sufficient skills, while using as little resources and time as possible, to gain maximum profit from the aquired skills".

I think what you really want to say is that you dislike cheating, no.

anders t wrote:
> The problem is that many of us who "must" learn Prolog will have only a
> few weeks to learn (and learn to like!) a completely new language (and
> most often a completely new paradigm). We encounter the language
> in a more or less compulsory course (often also including entry level
> theoretical AI which consumes education time!) in parallel with other
> tight courses.
> [...]
> We just don't have the time to invent the wheel again, to fiddle around
> and play with Prolog.

If you don't have time to play with Prolog, then you will never enjoy Prolog.

If you do not have time to write simple Prolog code, then you will not learn to write Prolog code without difficulty. Instead, you will only have Prolog assignments that are hard for you, you will never have the pleasure of writing Prolog code that you can get working easily.

Is there any point in "being taught" Prolog and only having assignments that you struggle with? If this is your only experience of Prolog, then of course you will not want to use Prolog again.

The only way to learn to write Prolog code is to practice using Prolog. Write simple Prolog code until you have the hang of it. Then you will enjoy Prolog, and will want to learn more.

> Like it or not but Prolog is to many of us an anomaly in
> the education path, or becomes, because of the real (or perceived) high
> threshold. We just don't see what the payback will be from whatever time
> we allocate to try to learn the language during those few weeks.

If sounds like your experiences of Prolog have not been good ones.

I taught myself Prolog, using Ivan Bratko's excellent book, and using a free Prolog interpreter that I downloaded. I mostly enjoyed the experience.

Perhaps when you have finished your course, if you have the time, you can teach yourself Prolog in the same way. Or instead of using Ivan Bratko's book, you can try working your way through the Prolog tutorial called "Learn Prolog Now!", this is good too.

But I suspect that the experiences that you have had with Prolog so far have not encouraged you.

(Details of the book by Ivan Bratko and the tutorial are in the FAQ for this newsgroup, if you want them.)

> Why don't the Prolog people/AI people (often the same, no?) use the 6-7
> weeks they have with thousands and thousands of students to buy them over
> to their paradigm by helping them over that threshold?

When you refer to "Prolog people", are you referring to University lecturers ?

I'm not a University person. I'm an amateur programmer using my home computer.

Should you be addressing your question to University lecturers who teach Prolog ?

> That would enable
> more of the students to drive deeper into Prolog and possibly finish the
> course with a desire to take that vital "2nd course".

Yes, if I was teaching an introductory course in Prolog at a University, I would try to give students a good introduction to the basics only. In an introductory course, I would not use Prolog lists at all, I would leave that for a second course, a more advanced course in Prolog.

> Again (yeah I'm today's parrot... :-) ): Is there really a desire within
> the Prolog Community to increase Prolog's popularity and usage?

I don't think that the Prolog Community as a whole has any desires.

I am an individual, not a community.

As an individual, I sometimes like to help people who send in questions to this discussion group. But I don't think that I have any way to increase Prolog's popularity. If I could increase Prolog's popularity, I would, but I don't know any way of doing that. So just think of me as someone who occasionally looks at this Prolog discussion group, and who answers questions here.

I'm not even sure if there really is a "Prolog community".

Now for a change of subject.

If someone sends in an easy Prolog question to this discussion group, I could send in the whole answer to his problem, and sometimes I have done that.

But if we do that for someone learning Prolog, for us to write the whole answer if not really a way to do a favour to a Prolog novice. All Prolog novices have to write Prolog code themselves, until they can do it without much difficulty, or they will never learn how to use Prolog, and they will never want to use Prolog.

I wasn't sure if the clue I gave to Yupar Nyo was enough for him to solve the problem. If he still can't solve the problem, that's OK, he can ask us again, and I can give him more clues. Or perhaps if he asks again, someone will send him the whole answer. My reply to Yupar was not meant to be final : if my clue was not enough to help him then I hope he will ask again.

anders t wrote:
> Quoting Andrzej Lewandowski in comp.lang.prolog:
>> Yes, but not by doing somebody's homework.
>
> I hope you understand at least in part where I'm coming from here.
>
> Put another way:
>
> Why don't the Prolog people/AI people (often the same, no?) use the 6-7
> weeks they have with thousands and thousands of students to buy them over
> to their paradigm by helping them over that threshold? That would enable
> more of the students to drive deeper into Prolog and possibly finish the
> course with a desire to take that vital "2nd course".

So are you suggesting that the "thousands and thousands of students" who are learning Prolog should swamp this newsgroup with trivial questions?

Or are you suggesting that people who teach Prolog do so in a way different from people who teach other sorts of programming? If so, I don't see any evidence of that. My experience of teaching any sort of programming is that students need to be encouraged to think through it themselves and that sometimes if they are show answers too early they never properly learn how to program.

Right now I am teaching a course in programming (not in Prolog however) and as an experiment I interviewed those stuents on the course who did badly on the mid-term test. I found a common feature of these students was an over-readiness to jump to model answers or to seek help without thinking it through first. When I asked these students to demonstrate their lab work, they showed me model answers they'd copied, and sometimes trivially modified and said "Oh, I looked through the answers and now I understand it". They didn't understand it - these are people who after a term and a half of learning to program (in Java actually) couldn't string together half a dozen lines of syntactically correct code that resembled a correct solution.

Quoting Matthew Huntbach in comp.lang.prolog:
> So are you suggesting that the "thousands and thousands of students" who are >learning Prolog should swamp this newsgroup with trivial questions?

No.

> Or are you suggesting that people who teach Prolog do so in a way different
> from people who teach other sorts of programming? If so, I don't see any
> evidence of that. My experience of teaching any sort of programming is that
> students need to be encouraged to think through it themselves and that
> sometimes if they are show answers too early they never properly learn how
> to program.
>
> Right now I am teaching a course in programming (not in Prolog however) and
> as an experiment I interviewed those stuents on the course who did badly on
> the mid-term test. I found a common feature of these students was an
> over-readiness to jump to model answers or to seek help without thinking it
> through first. When I asked these students to demonstrate their lab work,
> they showed me model answers they'd copied, and sometimes trivially modified
> and said "Oh, I looked through the answers and now I understand it". They
> didn't understand it - these are people who after a term and a half of
> learning to program (in Java actually) couldn't string together half a
> dozen lines of syntactically correct code that resembled a correct solution.

Generally, the guys who have responded to my various posts here, present thoughtful arguments and insights for which I thank.

While I, also in general, certainly agree that practical assignments is must in order to really learn, I must still highlight that the problem is that Prolog really is something new to anyone who has never dealt with declarative programming or, for that matter, heavy list programming.

We don't seem to get the time to let things mature. Especially in a combined AI/Prolog course we get 3-6 hours to learn how Prolog (I guess generally, declarative programming) works and then we are supposed to be off with solving (simpler) AI problems.

How many students start solving (simpler) AI problems or equivalents in OO programming after three hours of learning Java as a first OO language? There will of course always be geniuses who handle this perfectly, but geniuses alone can't support the Software market with the manpower needed.

Perhaps our brains are indeed destroyed by functional programming, but that's just another incentive to be more gentle with us students, in order to not repel us from Prolog/Declarative programming.

Also, it isn't helping us students that Prolog is diversified between (competing(??) implementations.

Noone has still not really answered my now (in)famous question (a bit rephrased):

Is there a true interest among Prolog theoreticists and practitioners to popularize Prolog and perhaps make it a mainstream language, like Java, C++, C#, or is there a desire to protect a territory? (I'm not necessarily saying that the latter would be something bad, I just want to establish an understanding.)

anders t wrote:
> Is there a true interest among Prolog theoreticists and practitioners to
> popularize Prolog and perhaps make it a mainstream language, like Java,
> C++, C#,

There's no consensus on how to "mainstream" Prolog, and no evidence that Prologists would devote significant effort to a common path rather than pursuing individual interests which tend to fragment, rather than strengthen, Prolog as a whole.

I find the Prolog FAQ depressing, with its list of proprietary and idiosyncratic implementations and extensions of Prolog, many of them dormant or defunct, with no viable way of combining their innovations. Indeed I doubt that any of them were developed with much regard to this: Prolog is currently much less than the sum of its parts.

Sadly, most of the creative Prologists are associated with exactly one (or other) of these implementations; perhaps we need some other focus, e.g. a neutral working group to develop APIs for embedding Prolog in other languages, in IDEs, in web app servers etc. Any nominations?

If we look at what has made RDBMSs so widely used and usable, a lot of it is not very sexy or theoretical, but mundane and necessary stuff for transactions, recovery, APIs for programmatic use etc, and it's not surprising that few want to contribute such work to Prolog while there is neither consensus on how this sort of stuff should be structured, nor even consensus on it being worth having at all.

Nevertheless, I haven't quite given up hope :-)

Paul Singleton wrote:
> anders t wrote:
>
>> Is there a true interest among Prolog theoreticists and practitioners to
>> popularize Prolog and perhaps make it a mainstream language, like Java,
>> C++, C#,
>
> There's no consensus on how to "mainstream" Prolog, and
> no evidence that Prologists would devote significant effort
> to a common path rather than pursuing individual interests
> which tend to fragment, rather than strengthen, Prolog as
> a whole.

This is a difficult topic with lots of different interrests. Commercial vendors have an interest to lock users into their system and non-commercial `vendors' have an interest in moving forward in terms of scientific contribution and/or pure functionality. Despite the clear common interrest of all maintainers of some implementation of the Prolog language it is a very hard task to get anything going.

Possibly one problem is that realisation of a simple implementation of the language is too easy, which let to too many of them :-)

I've tried to coordinate two attempts, but it turns out this really requires a fulltime job which I, like many of us, cannot affort as well as skills I do not posses. Standardisation should be at the top of our priority list, but it requires either a very strong partner (like W3C for the semantic web) or some sort of functioning decentralised infrastructure.

> Nevertheless, I haven't quite given up hope :-)

Good!

I think you should refer to the ISO standard for Prolog. All "mainstream" Prologs: IF/Prolog, SICStus Prolog etc do conform to this standard. There are a couple of industry exceptions PDC Prolog and LPA Prolog (please correct me if latest versions are now ISO conforming.)

The standard is a good one, it makes excellent definition of errors be they type or runtime errors. It also defines a good subset of predicates that provide all that you need.

Since the standard was completed there has been little or no need to modify it. Extending it to include modules and constraints was on the agenda, but never came to fruition.

Andrew R. Verden wrote:
> I think you should refer to the ISO standard for Prolog.

It would have been nice to quote some text, so we know to what you are refering.

> All "mainstream" Prologs: IF/Prolog, SICStus Prolog etc do
> conform to this standard. There are a couple of industry exceptions
> PDC Prolog and LPA Prolog (please correct me if latest versions are
> now ISO conforming.)
>
> The standard is a good one, it makes excellent definition of errors
> be they type or runtime errors. It also defines a good subset of
> predicates that provide all that you need.

There are many valid complaints on this standard. Nevertheless it is indeed adopted by almost all todays implementations which is a very good thing in itself. The trouble however is that its far too limited and it is still extremely hard to write even a very trivial program that runs on all these ISO compliant Prolog systems. What about a language without an accepted module system? Without a standard library? Without a standard interface to the outside world?

> Since the standard was completed there has been little or no need
> to modify it. Extending it to include modules and constraints was
> on the agenda, but never came to fruition.

Sadly ...

For the ISO Standard definition to Prolog please see www.iso.org search for Prolog.

There is also a modules definition which I think is very close to what IF/Prolog implements, but I am not 100% sure on this as I have not read the document. I also think this modules document has largely been ignored by the Prolog implementors and suppliers!

Overall though I do not believe Prolog is good as a mainstream language. It is very very good at modelling problems in a declaratve way and search strategies and compilers and parsing... In these areas it has been successful to a certain mainstream extent and is still used for all of these, even after some 20 years since the first commercial Prologs became available.

Many products also support Java APIs through easy interface definition or through auto-discovery. In any application development it is worth separating the GUI from the engine, and foreign API componenents should not be too deeply embedded into an application. Clear interfaces and modules help an application migrate through different platforms and GUIs and customers existing software.

This ease of compatibility is what makes it worth buying a decent Prolog system, in the same way one might buy a decent database. The decent vendor (us especially :-)) will continue to supply the future interfaces and try to stay one step ahead of what the users require.

It is not fair though to blame the Prolog langauge for its lack of interfacability into mainstream applications. The problem of finding a compatible set of componenets on compatible operating systems remains, regardless of whether or not Prolog is in the equation.

The computer industry as a whole has moved away from standardisation, at the expense of quality, and the benefit of speed to market. The ISO Prolog standard took more than 10 years to formulate and is one of the better standards, it actually re-used other standards usually standards have their own definition of an integer... see the C/C++ standard in comparison.

anders t wrote:
> Quoting Matthew Huntbach in comp.lang.prolog:
>> Or are you suggesting that people who teach Prolog do so in a way different
>> from people who teach other sorts of programming? If so, I don't see any
>> evidence of that. My experience of teaching any sort of programming is that
>> students need to be encouraged to think through it themselves and that
>> sometimes if they are show answers too early they never properly learn how
>> to program.
>
> While I, also in general, certainly agree that practical assignments is
> must in order to really learn, I must still highlight that the problem is
> that Prolog really is something new to anyone who has never dealt with
> declarative programming or, for that matter, heavy list programming.
>
> We don't seem to get the time to let things mature. Especially in a
> combined AI/Prolog course we get 3-6 hours to learn how Prolog (I guess
> generally, declarative programming) works and then we are supposed to be
> off with solving (simpler) AI problems.
>
> How many students start solving (simpler) AI problems or equivalents in OO
> programming after three hours of learning Java as a first OO language?
> There will of course always be geniuses who handle this perfectly, but
> geniuses alone can't support the Software market with the manpower needed.

Prolog is a very simple language. There isn't a huge amount of syntactical constructs to master. The basics of Prolog programming *can* be put across very simply in a few hours. After that, what else is there to do but to go through examples, and my experience is that going through examples by doing them yourself is the only way to really learn. In a language like Java there are a lot more constructs to learn - you have to explain variables, then the procedural structures, then methods, then objects, them inheritance. Obviously this is going to take longer than it takes to explain the little bit of syntax and operatonal behaviour that is all Prolog is. So I think learning Prolog is better compared to learning just one aspect of Java. For example, the basic control flow aspects of Java should certainly be learnable to the point where students would be expected to solve siple problems in them in the space of 3-6 hours.

> Perhaps our brains are indeed destroyed by functional programming, but
> that's just another incentive to be more gentle with us students, in order
> to not repel us from Prolog/Declarative programming.

When you say "functional programming" I assume you actually mean "procedural programming", since functional programming is another form of declarative programming. Perhaps it depends on how you have been taught programming previously. Many people seem to find recursion incredibly difficult to handle, and this is the basis for them finding Prolog difficult since in Prolog you can't escape from using recursion. But recursion can be taught in other languages. When I teach Java, I give my students a simple list abstract data type, and get them to write simple-list handling programs similar to those one would write in Prolog. I'd expect them to be able to do this after a few hours teaching them about lists and recursion, so I don't see that as much different to what you say about learning Prolog.

> Also, it isn't helping us students that Prolog is diversified between
> (competing(??) implementations.

In what way? The basics of Prolog do not alter between the various implementations, and surely its these basics that a novice Prolog programmer is going to be dealing with. I would not expect the sort of programs a novice Prolog programmer would write to be any different no matter what implementation is being used.

> Noone has still not really answered my now (in)famous question (a bit
> rephrased):
>
> Is there a true interest among Prolog theoreticists and practitioners to
> popularize Prolog and perhaps make it a mainstream language, like Java,
> C++, C#, or is there a desire to protect a territory? (I'm not necessarily
> saying that the latter would be something bad, I just want to establish an
> understanding.)

No, clearly not. How on earth would it serve anyone who wants to promote a language to deliberately try and put people off it? What a ridiculous point you are making here.

I don't think Prolog is competing to be a mainstream language because I think it has flaws that mean it can't be. It has been around a long time, and it's a tribute to its very simple elegant design that it hasn't changed much since first introduced and all attempts to introduce more complex but "better" logic languages haven't really succeeded. However, I don't think it really scales up to what is required to produce large scale software for modern computing systems. So I think it's something best taught as an interesting idea that helps get you thinking and is worth a few hours on the curriculum, rather than as a major topic you are going to need to become a real expert in and spend many long hours learning.

Matthew Huntbach wrote:
> I don't think Prolog is competing to be a mainstream language
> because I think it has flaws that mean it can't be.

Could you please explain which flaws? Because I can't see them...

Such things as the lack of a type system, lack of a module system, poor handling of interaction ...

/* n_solutions.pl by Tom Breton, 27 Feb 2004, Copylefted under terms
of the Gnu Public License. */

%%Impure, non-declarative, but gets the job done.

%%Find no more than N solutions of the predicate Goal.
%%Since standard Prolog has no lambda, we use `Var' + `Goal' form.
n_solutions(Var,Goal,All_sols,N) :-
        gensym(found,Key),
        limited_try(Var,Goal,Key,N),
        %%Collect the recorded solutions into `All_sols'.
        findall(Solution, recorded(Key,Solution), All_sols),
        %%Clean up the database.
        eraseall(Key).
%%Solution is a variable in `Goal' that one wants to store.
%%Since standard Prolog has no lambda, we use `Var' + `Goal' form.
%%`Key' must be suitable for recordz/2.
%%Solutions are returned in the database as
%%`recorded(Key,A_solution)'.

limited_try(Solution,Goal,Key,N) :-
        %%Probably no reason for caller to use N = 0 etc, but catch it
        %%anyways.
        (N =< 0) -> true
        ;
        ((
          %%The engine.
          Goal,
          %%Record the solution.  `Goal' and `Solution' had to be
          %%linked together by caller.
          recordz(Key,Solution),
          (

            %%If there's already a surfeit of solutions, stop searching
            %%and discard Goal's remaining choice-points.
            (num_keyed_records(Key,Num_sols), (Num_sols >= N)) -> !
          ;
            %%Otherwise keep looking, by failure-driven loop
            fail))
        ;

    %%Use of failure-driven loop risks making success/failure confusing to
    %%the caller. So a final branch always succeeds and allows no
    %%choice-point.
    !).


num_keyed_records(Key,Num_sols) :-
        findall([], recorded(Key,_), All_sols),
        length(All_sols, Num_sols).

eraseall(Key) :-
        (recorded(Key, _, Reference), erase(Reference)) ->
        eraseall(Key)
        ;
        true.

You can do that using the `do_while' predicate in the `std_util' module. That predicate lets you use any condition you like to decide when to stop finding solutions -- for example you can decide to stop based on the number of solutions found so far, based on user input, or even based on the time of day.
I have enclosed an example below.

%------------------------------------------------------------%

% An example program to illustrate the use of the `do_while'
% predicate in Mercury.  This program calls a nondeterministic
% predicate hello/1, and prints the first N solutions it finds
% (in this case for N = 2).

:- module n_solutions.
:- interface.
:- import_module io.

:- pred main(io__state::di, io__state::uo) is cc_multi.

:- implementation.
:- import_module std_util, bool, int.

main(!IO) :-
        N = 2,
        do_while(hello, get_next, {!.IO, N}, {!:IO, _}),
        print("Done\n", !IO).

:- pred hello(string::out) is multi.

hello("Hello, world\n").
hello("Good day, world\n").
hello("Greetings, world\n").

:- pred get_next(string::in, bool::out, {io, int}::di, {io, int}::uo)
        is det.

get_next(String, More, {IO0, Max0}, {IO, Max}) :-
        print(String, IO0, IO),
        More = (Max0 > 1 -> yes ; no),
        Max = Max0 - 1.

Isn't this rather, er, non-logical for Mercury? And, at the risk of getting flamed :-), doesn't this mean that you can simulate the effect of the Prolog "cut" in Mercury? I thought that Mercury was striving to be more logical than that.

I think the term you're looking for is "referentially transparent" or "pure".

If I understand right, no, the call to `do_while/4' can be replaced by its results (ie, the unifications that result) and the behavior will be the same.

Fergus Henderson wrote:
> You can do that using the `do_while' predicate in the `std_util' module.
> That predicate lets you use any condition you like to decide when to
> stop finding solutions -- for example you can decide to stop based on the
> number of solutions found so far, based on user input, or even based on
> the time of day.

Jamie Andrews writes:
> Isn't this rather, er, non-logical for Mercury? And, at
> the risk of getting flamed :-), doesn't this mean that you can
> simulate the effect of the Prolog "cut" in Mercury? I thought
> that Mercury was striving to be more logical than that.

Mercury strives to be practical as well as referentially transparent, which is why we have developed mechanisms that often allow us to achieve both objectives at the same time. Do_while is declared to be cc_multi, which means that its declarative semantics says that it may have many solutions, but its operational semantics will compute just one. The comment at the start of do_while's definition in the Mercury standard library describes both semantics:

        % This is a generalization of unsorted_aggregate which allows the
        % iteration to stop before all solutions have been found.
        % Declaratively, the specification is as follows:
        %
        %       do_while(Generator, Filter) -->
        %               { unsorted_solutions(Generator, Solutions) },
        %               do_while_2(Solutions, Filter).
        %
        %       do_while_2([], _) --> [].
        %       do_while_2([X|Xs], Filter) -->
        %               Filter(X, More),
        %               (if { More = yes } then
        %                       do_while_2(Xs, Filter)
        %               else
        %                       { true }
        %               ).
        %
        % Operationally, however, do_while/4 will call the Filter
        % predicate for each solution as it is obtained, rather than
        % first building a list of all the solutions.

Since do_while is cc_multi (as is unsorted_solutions), it can only be called in a committed choice context ("cc" means "committed choice"), i.e. a context in which a goal may have more than one solution to choose from, but the execution will commit to one of those solutions. There are only three ways you can create a committed choice context.

The first way is if main is also cc_multi. In this case, the declarative semantics of the program as a whole may have more than one solution, while operationally, an execution of the program will return one of these. There are compiler options that allow programmers to control which solution this is.

The second way is a goal that may have more than one solution has all its output variables existentially quantified away; the usual case where this occurs is when the condition of an if-then-else checks whether a collection (list, set, etc) has an element with a specific property. In this case, all we care about is whether a solution exists or not; the bindings associated with the solution are immaterial.

The third way is explicit use of a builtin predicate such as promise_only_solution, which is effectively a determinism cast that allows the rest of the program to treat a cc_multi computation as if it were a deterministic (det) computation.

The first two ways preserve the declarative semantics of the program. The third is basically an assertion by the programmer that he/she is relying on the operational semantics, and wishes to build the declarative semantics of the surrounding code on the operational semantics, not the declarative semantics, of the code inside the determinism cast.

Determinism casts are intended to be used only by experts, and only when necessary. The Mercury compiler has roughly ten thousand predicates, and only ten occurrences of promise_only_solution. I don't have hard data on the frequency of cuts in large-scale Prolog programs, but it is safe to bet that it is a lot more than one per thousand predicates.

Tom Breton writes:
> If I understand right, no, the call to `do_while/4' can be replaced by
> its results (ie, the unifications that result) and the behavior will
> be the same.

That is correct, but that is not by itself sufficient to give do_while a declarative semantics.

Zoltan Somogyi wrote:
> Since do_while is cc_multi (as is unsorted_solutions), it can only be called
> in a committed choice context ("cc" means "committed choice"), i.e. a context
> in which a goal may have more than one solution to choose from, but the
> execution will commit to one of those solutions. There are only three ways
> you can create a committed choice context.
> The first way is if main is also cc_multi. In this case, the declarative
> semantics of the program as a whole may have more than one solution,
> while operationally, an execution of the program will return one of these....
> The second way is a goal that may have more than one solution has all its
> output variables existentially quantified away; ...

I don't think that either of these is what the original poster (Tom Breton) wanted; he seemed to want something that would return no more than N solutions, and then go on computing as if those were the only solutions. For instance, if p(X) returned first X=a, then X=b, then X=c on backtracking, he seemed to want a construct "foo" such that foo(p(X), 2) would return just X=a and X=b; so that the goal "foo(p(X), 2), X=c" would fail even though "p(X), X=c" is true declaratively. But I could have misinterpreted what he wanted.

> The third way is explicit use of a builtin predicate such as
> promise_only_solution, which is effectively a determinism cast
> that allows the rest of the program to treat a cc_multi computation
> as if it were a deterministic (det) computation....
> Determinism casts are intended to be used only by experts, and only when
> necessary.

Hmm... I say the same thing about assert and retract... that doesn't seem to stop Prolog learners from jumping to the conclusion that theirs is the one case in a million where they really need assert/retract... but I take your point that this is flagged in the documentation as a "bad thing" that shouldn't have to be used by anyone for most ordinary applications. Still, I find it interesting that you came to the conclusion that this equivalent of a "red cut" is necessary for practical purposes in some cases.

> The Mercury compiler has roughly ten thousand predicates,
> and only ten occurrences of promise_only_solution. I don't have hard data
> on the frequency of cuts in large-scale Prolog programs, but it is safe
> to bet that it is a lot more than one per thousand predicates.

A closer comparison would be to cuts that are not negation-replacement cuts (put in in order to avoid calling a predicate again in a later clause with "not" in front of the call), but which still alter the solutions returned. It's safe to bet that this also is more than one per thousand predicates, but it could be lower than one per 100 predicates. A careful Prolog programmer will have as little reason to do this in most cases as a Mercury programmer. The difference between one in 100 and one in 1000 is probably due to errors on the part of the Prolog programmer.

The value of the Mercury mode and determinism system is that we are able to enlist the help of the compiler in finding such errors. The Prolog programmer is totally on their own (well, with their trusty copy of O'Keefe by their side), and probably often fails to find them.

However, it seems that no pragmatic language can achieve the goal of being 100% declarative. Prolog systems, having been designed in the late 70s and early 80s, set the bar lower than Mercury, but Mercury still doesn't set the bar at 100%.

I wrote:
> The first way is if main is also cc_multi. In this case, the declarative
> semantics of the program as a whole may have more than one solution,
> while operationally, an execution of the program will return one of these....
> The second way is a goal that may have more than one solution has all its
> output variables existentially quantified away; ...

Jamie Andrews writes:
> I don't think that either of these is what the original
> poster (Tom Breton) wanted;

I don't think so either. I just mentioned them as part of my "thorough response" to show that committed choice contexts are always declarative unless the programmer says he/she explicitly wants to use them in an operational manner.

> The value of the Mercury mode and determinism system is
> that we are able to enlist the help of the compiler in finding
> such errors.

Yes, exactly. When Mercury was new, lots of people were impressed by its speed, but few seemed to believe us when we said that the type, mode and determinism systems were there more to help programmers find bugs than to help the compiler generate fast code.

> However, it seems that no pragmatic language can achieve
> the goal of being 100% declarative. Prolog systems, having been
> designed in the late 70s and early 80s, set the bar lower than
> Mercury, but Mercury still doesn't set the bar at 100%.

I don't think you can set the bar to 100% and still get performance comparable to imperative languages on today's von Neumann architectures, except for some specialized domains (e.g. number crunching in Sisal). Relaxing the target from 100% to 99% can make a significant difference in performance (for example, it is a lot easier to build a fast ML implementation than a fast implementation of Haskell). As long as the impure parts are hidden behind abstraction barriers with declarative interfaces, you don't lose the benefits of being purely logical in the rest of the system.

Jamie Andrews wrote:
> I don't think that either of these is what the original
> poster (Tom Breton) wanted; he seemed to want something that
> would return no more than N solutions, and then go on computing
> as if those were the only solutions.

Correct, but when Fergus described the `do_while' predicate, that gave me what I wanted.

Jamie Andrews wrote:
> Isn't this rather, er, non-logical for Mercury? And, at
> the risk of getting flamed :-), doesn't this mean that you can
> simulate the effect of the Prolog "cut" in Mercury? I thought
> that Mercury was striving to be more logical than that.

Not at all! Mercury supports committed choice nondeterminism wherein you only get *one* of the possible solutions to a nondeterministic goal. In order to ensure the declarative semantics of the program are preserved, you are not allowed to backtrack into a committed choice procedure, which in practice makes their use somewhat restrictive. However, there are situations such as with do_while where the alternative (in this case enumerating all solutions, sorting them, then choosing a prefix of the resulting list to process) is unacceptably costly.

This is quite different to Prolog's cut operator which really can (and usually does) destroy the declarative reading of a program.

• TPLP regular papers
• Transactions On Computational Logic (TOCL) regular papers

TECHNICAL NOTES

• Speedup of Logic Programs by Binarization and Partial Deduction.
  Jan Hruza, Petr Stepanek

PROGRAMMING PEARL

• Enhancing a search algorithm to perform intelligent backtracking. [CoRR]
  Maurice Bruynooghe

• Computing convex hulls with a linear solver. [CoRR]
  Florence Benoy, Andy King, and Fred Mesnard

REGULAR PAPERS

• Weight constraints as nested expressions. [CoRR]
  Paolo Ferraris and Vladimir Lifschitz

• A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages.
  Patricia M. Hill, Enea Zaffanella, and Roberto Bagnara

• Abduction in well-founded semantics and generalized stable models via tabled dual programs.
  Jose Alferes, Luis Moniz Pereira, and Terrance Swift

• Applications of intuitionistic logic in answer set programming. [CoRR]
  Mauricio Osorio Galindo, Juan Antonio Navarro Perez, Jose Arrazola

• XPath-Logic and XPathLog: a logic-programming-style XML data manipulation language. [CoRR]
  Wolfgang May

• A Proof Theoretic Approach to Failure in Functional Logic Programming.
  Francisco Javier Lopez-Fraguas and Jaime Sanchez-Hernandez

• Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf.
  Andrew W. Appel and Amy P. Felty

• Computing stable models: worst-case performance estimates. [CoRR]
  Zbigniew Lonc and Miroslaw Truszczynski

• Minimal founded semantics for disjunctive logic programs and deductive databases. [CoRR]
  Filippo Furfaro, Gianluigi Greco and Sergio Greco

• Defeasible Logic Programming: An Argumentative Approach. [CoRR]
  Alejandro Javier Garcia and Guillermo Ricardo Simari

• Offline specialisation in Prolog using a hand-written compiler generator. [CoRR]
  Michael Leuschel, Jesper Jorgensen, Wim Vanhoof, Maurice Bruynooghe

• Logic-Based Specification Languages for Intelligent Software Agents. [CoRR]
  Viviana Mascardi, Maurizio Martelli and Leon Sterling

• On Applying Or-Parallelism and Tabling to Logic Programs. [CoRR]
  Ricardo Rocha, Fernando Silva, Vitor Santos Costa

• Enhanced sharing analysis techniques: a comprehensive evaluation.
  Roberto Bagnara, Enea Zaffanella, Patricia M. Hill

• Transformations of logic programs with goals as arguments. [CoRR]
  Alberto Pettorossi, Maurizio Proietti

The files below are the final versions of the papers submitted by the authors. The definite, published versions of the papers are available from the TOCL home page within the ACM Digital Library.

• Automatic Generation of Rule-based Constraint Solvers over Finite Domains, Slim Abdennadher and Christophe Rigotti
• A Logic Programming Approach to Knowledge-State Planning: Semantics and Complexity, Thomas Eiter, Wolfgang Faber, Nicola Leone, Gerald Pfeifer, and Axel Polleres
• Convergent Approximate Solving of First-Order Constraints by Approximate Quantifiers, Stefan Ratschan
• Inflationary Fixed Points in Modal Logic, Anuj Dawar, Erich Grädel, and Stephan Kreutzer
• Optimal Length Tree-like Resolution Refutations for 2SAT formulas, K. Subramani
• Classes of Term Rewrite Systems with Polynomial Confluence Problems, Guillem Godoy, Ashish Tiwari and Robert Nieuwenhuis
• Some applications of logic to feasibility in higher types, Aleksandar Ignjatovic and Arun Sharma
• A Decomposition-Based Implementation of Search Strategies, Laurent Michel and Pascal Van Hentenryck

• Basic Theory of Feature Trees, P. Mielniczuk
• Finite state machines for strings over infinite alphabets, F. Neven, T. Schwentick and V. Vianu
• Symbolic Semantic Rules for Producing Compact STGLA from Value Passing Process Descriptions, Marco Bernardo
• Termination of Simply Moded Logic Programs with Dynamic Scheduling, Annalisa Bossi, Sandro Etalle, Sabina Rossi and Jan-Georg Smaus
• Hypotheses-Based Semantics of Logic Programs in Multi-Valued Logics, Yann Loyer, Nicolas Spyratos and Daniel Stamate
• Reflective Metalogical Frameworks, David Basin, Manuel Clave and Jose Meseguer

• A theory of normed simulations, W.O.D. Griffioen and F.W. Vaandrager
• Abstract versus Concrete Computation on Metric Partial Algebras, J.V. Tucker and J.I. Zucker
• NExpTime-complete Description Logics with Concrete Domain, Carsten Lutz
• Proving correctness of Timed Concurrent Constraint Programs, Frank de Boer, Maurizio Gabbrielli and Maria Chiara Meo
• Interval Constraint Solving for Camera Control and Motion Planning, Frederic Benhamou, Frederic Goualard, Eric Languenou and Marc Christie
• A Classification of Symbolic Transition Systems, T.A. Henzinger, R. Majumdar and J.-F. Raskin
• Making Abstract Domains Condensing, R. Giacobazzi, F. Ranzato and F. Scozzari
• On Equivalence and Canonical Forms in the LF Type Theory, Robert Harper and Frank Pfenning
• A New Decidability Technique for Ground Term Rewriting Systems with Applications, Rakesh Verman and Ara Hayrapetyan
• A Modal Logic Framework for Multi-agent Belief Fusion, Churn-Jung Liau
• Eternity variables to prove simulation of specifications, Wim H. Hesselink
• Induction from answer sets in nonmonotonic logic programs, Chiaki Sakama
• Complexity of Nested Circumscription and Nested Abnormality Theories, Marco Cadoli, Thomas Eiter and Georg Gottlob
• From Linear Time to Branching Time, Orna Kupferman and Moshe Vardi
• Comparisons and Computation of Well-founded Semantics for Disjunctive Logic Programs, Kewen Wang and Lizhi Zhou
• Equivalences Among Aggregate Queries with Negation, Sara Cohen, Werner Nutt and Yehoshua Sagiv
• Knuth-Bendix constraint solving is NP-complete, Konstantin Korovin and Andrei Voronkov
• Reasoning about Evolving Nonmonotonic Knowledge Bases, Thomas Eiter, Michael Fink, Giuliana Sabbatini and Hans Tompits
• Minimum Model Semantics for Logic Programs with Negation-as-Failure, Panos Rondogiannis and William W. Wadge
• Datalog programs and their persistency numbers Foto Afrati, Stavros Cosmadakis and Eugenie Foustoucos
• On the Complexity of the Disjunction Property in Intuitionistic and Modal Logics Mauro Ferrari, Camillo Fiorentini and Guido Fiorino
• Disjunction and Modular Goal-directed Proof Search Matthew Stone
• Sequent and Hypersequent Calculi for Lukasiewicz and Abelian Logics George Metcalfe, Nicola Olivetti, and Dov Gabbay
• An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables Bernard Boigelot, Sebastien Jodogne and Pierre Wolper
• Arithmetic, First-Order Logic, and Counting Quantifiers Nicole Schweikardt
• Unfolding Partiality and Disjunctions in Stable Model Semantics T. Janhunen, I. Niemela, D. Seipel, P. Simons and J. You
• Predicate-calculus based logics for modeling and solving search problems Deborah East and Mirek Truszczynski
• Complexity Results on DPLL and Resolution Paolo Liberatore

The design of the new logic programming language is influenced by the need for an efficient implementation, which is reasonable given the near-term requirements. But there can also be value in taking a long-term view, as Paul Graham suggests in "The Hundred-Year Language" (http://www.paulgraham.com/hundred.html). We should ask ourselves, what would the ideal language be if efficiency was not a consideration?

This article proposes such a language. The language objectives are

1. a pure-specification language -- implementation is ignored,
2. minimal, but extensible -- nothing is built-in, and
3. a meta-language -- able to imitate and thus subsume other languages.

The language, called "axiomatic language", is based on the idea that the external behavior of any function or program, even an interactive program, can be represented by a static infinite set of symbolic expressions that enumerate all possible inputs, or sequences of inputs, along with the corresponding outputs. Thus the language is just a formal system for generating these symbolic expressions. Axiomatic language can be described as pure, definite Prolog with Lisp syntax, plus HiLog higher-order generalization, plus "string variables", which match a string of expressions in a sequence. Details and examples can be found at www.axiomaticlanguage.org.

I believe the various features being considered for the new LP language (constraints, types, modules, etc.) can be defined within this much simpler language using its extensibility. The papers on the language website show how Lisp-like expression evaluation and even a simple procedural language can be defined. Thus debates over language features would become debates over what to put in a library.

The challenge, of course, is to automatically generate efficient programs from specifications. Hopefully it won't take 100 years! Perhaps human-aided program synthesis is a practical intermediate goal.

A consensus on a long-term LP language would provide a target which might benefit the current NLPL design and might help focus research on program transformation. The language may also be useful as a non-executable language for software specification.

PADL is an excellent forum for researchers and practioners to present and discuss original work on novel applications and implementation techniques for all forms of declarative concepts emerging from functional, logic, and constraint programming paradigms.
PADL 2004 features 15 contributed papers and two invited talks - by Paul Hudak (Yale) and Andrew Fall (Dowlland Technologies and Simon Fraser).
The conference is preceeded by a four-day Summer School (June 14-17). PADL is organized in cooperation with COMPULOG USA and the Association for Logic Programming. The symposium proceedings are published by Springer Verlag as part of its Lecture Notes in Computer Science series.

______________________________________________________________________
			DAY 1: FRIDAY, JUNE 18
______________________________________________________________________


8:00 - 9:00:  Breakfast and Registration

9:00 - 9:10:  Welcome and Opening Remarks

9:10 - 10:10: INVITED TALK - PAUL HUDAK, Yale University

	      "An Algebraic Theory of Polymorphic Temporal Media"

10:15 - 10:30: Break

______________________________________________________________________

10:30 - 12:30: TYPE SYSTEMS AND FUNCTIONAL PROGRAMMING - Session I

"A Typeful Approach to Object-Oriented Programming with Multiple Inheritance"
Chiyan Chen, Rui Shi, and Hongwei Xi,
Boston University, USA

"Compositional Model-Views with Generic Graphical User Interfaces"
Peter Achten, Marko van Eekelen, Rinus Plasmeijer, 
                      University of Nijmegen, The Netherlands

"An Implementation of Session Types"
Matthias Neubauer and Peter Thiemann,
Universitat Freiburg, Germany

"UUXML: A Type-Preserving XML Schema-Haskell Data Binding"
Frank Atanassow, Dave Clarke, and Johan Jeuring, Utrecht University, The Netherlands

______________________________________________________________________

12:30 - 2:00: LUNCH 


2:00 - 3:30: IMPLEMENTATION OF LOGIC PROGRAMS

"Improved Compilation of Prolog to C Using Moded Types and Determinism Information" 
J. Morales, Manuel Carro, and Manuel Hermenegildo (*), 
            Technical University of Madrid and (*) University of New Mexico

"A Generic Persistence Model for (C)LP Systems 
	(and two useful implementations)"
J. Correas, J.M. Gomez, M. Carro, D. Cabeza, and M. Hermenegildo (*), 
            Technical University of Madrid and (*) University of New Mexico

"Pruning in the Extended Andorra Model"
Ricardo Lopes, Vitor Santos Costa (*), and Fernando Silva 
            University of Porto, Portugal
(*) Universidade Federale do Rio de Janeiro, Brazil

______________________________________________________________________

3:30 - 4:00: BREAK

4:00 - 5:00: ANSWER SET PROGRAMMING

"USA-Smart: Improving the Quality of Plans in Answer Set Planning"
Marcello Balduccini, Texas Tech University, USA

"ASP-Prolog: A System for Reasoning about Answer Set Programs in Prolog"
Omar Elkhatib, Enrico Pontelli, and Tran Cao Son, New Mexico State University, USA

7:00: CONFERENCE DINNER



______________________________________________________________________
			DAY 2: SATURDAY, JUNE 19
______________________________________________________________________

8:00 - 9:00: Breakfast 

9:00 - 10:00: INVITED TALK - ANDREW FALL, 
	      Gowlland Technologies and Simon Fraser University,

	      "Supporting Decisions in Complex, Uncertain Domains with 
	      Declarative Languages" 

10:00 - 10:30 Break

______________________________________________________________________

10:30 - 12:00: DECLARATIVE PROGRAMMING

"Simplifying Dynamic Programming via Tabling" 
(Selected by the Program Committee for the 'Most Practical Paper' Award) 
Hai-Feng Guo, University of Nebraska at Omaha Gopal Gupta, University of Texas at Dallas

"Symbolic Execution of Behavioral Requirements"
Tao Wang, Abhik Roychoudhury, Roland H.C. Yap, and S.C. Choudhary National 
             University of Singapore, Singapore
 
"Observing Functional Logic computations"
Bernd Brassel, Olaf Chitil (*), Michael Hanus, and Frank Huch 
             Institut for Informatik, Kiel, Germany (*) University of Kent, Canterbury, U.K.

______________________________________________________________________

12:00 - 1:30: LUNCH

1:30 - 3:00: TYPE SYSTEMS - Session II

"Parametric Fortran - A Program Generator for Customized Generic Fortran Extensions" 
Martin Erwig and Zhe Fu, Oregon State University, USA

"Typing XHTML Web Applications in ML"
Martin Elsman and Ken Friis Larsen
IT University of Copenhagen, Denmark

"Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell" 
Chiyan Chen, Dengping Shu, and Hongwei Xi Boston University, USA

ACCEPTED PAPERS:

• S. Antoy, S. Johnson: TeaBag: A Functional Logic Language Debugger
• M. Garcia-Diaz, S. Nieva: A Fixed Point Semantics for an Extended CLP Language
• J.M. Cleva, J. Leach, F.J. Lopez-Fraguas: A logical approach to the verification of functional-logic programs
• M. Hanus: Dynamic Predicates in Functional Logic Programs
• M. Alpuente, M. Falschi, A. Villanueva: Symbolic Representation of tccp Programs
• B. Braßel, M. Hanus, F. Huch: Encapsulating Non-Determinism in Functional Logic Computations
• W. Lux: Comparing Copying and Trailing Implementations for Encapsulated Search
• H. Simoes, M. Florido: TypeTool: A Type Inference Visualization Tool
• C. Lembeck, R. Caballero, R.A. Müller, H.Kuchen: Constraint Solving for Generating Glass-Box Test Cases

Accepted Papers:

• Constraint Handling Rules and Tabled Execution, Tom Schrijvers, David S. Warren
• Smodels with CLP and its Applications: A Simple and Effective Approach to Aggregates in ASP, Islam Elkabani, Enrico Pontelli, Son Cao Tran
• Compiling Prioritized Circumscription into Answer Set Programming,Toshiko Wakaki, Katsumi Inoue
• Compiling Ask Constraints, Gregory J. Duck, Maria Garcia de la Banda, Peter J. Stuckey
• On Programs with Linearly Ordered Multiple Preferences, Davy Van Nieuwenborgh, Stijn Heymans, Dirk Vermeir
• Possible Worlds Semantics for Probabilistic Logic Programs, Alex Dekhtyar, Michael I. Dekhtyar
• Limiting Resolution: from Theory to Implementation, Patrick Caldon, Eric Martin
• The Real Operational Semantics of Constraint Handling Rules, Gregory J. Duck, Peter J. Stuckey, Maria Garcia de la Banda, Christian Holzbaur
• Logic Programs with Annotated Disjunctions, Joost Vennekens, Sofie Verbaeten, Maurice Bruynooghe
• Splitting an Operator: An Algebraic Modularity Result and its Applications to Logic Progamming, Joost Vennekens, David Gilis, Marc Denecker
• Simplifying Logic Programs under Answer Set Semantics, David Pearce
• Improving Prolog Programs: Refactoring for Prolog, Tom Schrijvers, Alexander Serebrenik
• Fast Query Evaluation with (Lazy) Control Flow Compilation, Remko Troncon, Gerda Janssens, Henk Vandecasteele
• Abstract Domains Based on Regular Types, John P. Gallagher, Kim S. Henriksen
• On Hybridization of Local Search and Constraint Propagation, Eric Monfroy, Frédéric Saubion, Tony Lambert
• Generalised Kernel Sets for Inverse Entailment, Oliver Ray, Krysia Broda, Alessandra Russo
• Speculative Computations in Parallel Tabled Logic Programs, Ricardo Rocha, Fernando Silva, Vitor Santos Costa
• Enhancing the Magic-Set Method for Disjunctive Datalog Programs, Chiara Cumbo, Wolfgang Faber, Gianluigi Greco, Nicola Leone
• alpha-Prolog: A Logic Programming Language with Names, Binding and alpha-Equivalence, James Cheney, Christian Urban
• Implementation Results in Classical Constructive Negation, Susana Muñoz, Juan José Moreno-Navarro
• Rectilinear Steiner Tree Construction using Answer Set Programming, Esra Erdem, Martin D. F. Wong
• Multi-agent Coordination as Distributed Logic Programming, David Robertson
• On Acyclic and Head-Cycle Free Nested Logic Programs, Thomas Linke, Hans Tompits, Stefan Woltran
• Adding domain dependent knowledge to answer set programs for planning, Xiumei Jia, Jia-Huai You, Li Yan Yuan
• Arc-consistency + unit propagation = lookahead, Jia-Huai You, Guiwen Hou
• The Period Constraint, Nicolas Beldiceanu, Emmanuel Poder
• Non-Viability Deductions in Arc-Consistency Computation, Frank D. Valencia
• Termination of Logic Programs for Various Dynamic Selection Rules, Jan_Georg Smaus

Following the panel discussion at ICLP 2003 in Mumbai (India) the first international workshop on Teaching Logic Programming TeachLP 2004 will be held in Saint Malo, France. The meeting will be run as a workshop at the 2004 International Conference on Logic Programming, which will be held on September 6-10, 2004.

Logic Programming and Constraint Logic Programming (LP, CLP) are very powerful programming paradigms, but hard to learn without sufficient help. For further spreading the technology it should be taught to a broader range of computer science students. The workshop will investigate what is currently taught and how; it will also discuss what should be taught and why. Suggested topics for submissions include, but are not limited to:

• teaching on different aspects of (C)LP
  • the fundamentals of logic programming
  • software engineering techniques for Prolog
  • debugging techniques for Prolog
  • practical applications
• teaching special aspects of (C)LP, such as
  • control structures
  • meta predicates
• teaching Prolog/(C)LP in a few hours for CS students
• tools for teaching
  • tools for teaching (C)LP
  • using (C)LP technology for e-learning systems
• relation to other fields
  • (C)LP in relation to other paradigms
  • applying (C)LP in other courses
• (C)LP and the ACM curriculum
• (C)LP for the masses or for experts

The workshop is planned to be half a day, with presentations of 30 minutes. A fundamental goal is to give opportunities for active discussions on new research directions and the exchange of latest results.

Organizing Committee

• Dietmar Seipel (Univ. Wuerzburg, Germany)
• Mireille Ducasse (IRISA/INSA de Rennes, France)
• Ulf Nilsson (Linkopings Univ., Linkoping, Sweden)

Important Dates

• Submission deadline: June 20, 2004
• Notification of acceptance: July 19, 2004
• Camera ready version: August 11, 20

Submissions

UNIF is the main international meeting on unification. Unification is concerned with the problem of identifying given terms, either syntactically or modulo a given logical theory. Syntactic unification is the basic operation of most automated reasoning systems, and unification modulo theories can be used, for instance, to build in special equational theories into theorem provers.

The aim of UNIF 2004, as that of the previous meetings, is to to bring together people interested in unification, present recent (even unfinished) work, and discuss new ideas and trends in unification and related fields. In particular, it is intended to offer a good opportunity for young researches and researchers working in related areas to get an overview of the current state of the art in unification theory and get in contact with the experts in the field.

Topics of Interest:

• Unification
• E-unification
• Unification Algorithms
• Higher-Order Unification
• String Unification
• Context Unification
• Combination problems
• Disunification
• Typed Unification
• Related Topics
• Constraint Solving
• Tree Descriptions
• Matching
• Narrowing
• Applications
• Type Checking and Type Inference
• Automated Deduction
• Rewriting
• Functional and Logic Programming
• Grammars
• Computational Linguistics
• Implementations

IMPORTANT DATES:

  Deadline for electronic submission:   Friday, May 14, 2004
  Notification of acceptance:                 Monday, May 24, 2004
  Deadline for camera-ready papers:    Monday, June 7, 2004
  Workshop:                                          July 4 - 5, 2004

UNIF 2004 SUBMISSIONS:
Authors are invited to submit via email an abstract (1-5 pages), a paper (no longer than 15 pages), or a system description (no more than 5 pages) in Postscript or PDF format to:
           unif04@iu-bremen.de
before May 14, 2004. Authors are encouraged to use LaTeX2e and the Springer llncs class. Accepted papers, abstracts and system descriptions will be included in the proceedings which will be available at the workshop.

• Five tutorials:
• General overview of Oz and Mozart with highlights
• Teaching programming with Oz
• Constraint programming in Oz
• Distributed programming in Oz
• Practical tips on industrial deployment
• Invited speaker (to be announced)
• Research paper sessions
• Application demonstration and poster sessions
• Panel discussion on the future of Mozart/Oz
• Vendor sessions

• frameworks for security using algorithms
• verification techniques
• process algebras
• programming languages with a Constraint or Logic Programming flavour
• techniques for writing secure programs
• POLA (Principle Of Least Authority) application
• Capabilities

In the last ten years, much progress has been made in our ability to solve problems in propositional satisfiability (or SAT) and related areas. In 2000, a very successful special issue of the Journal of Automated Reasoning and an accompanying book documented the progress made up to that time. In the subsequent five years, even more dramatic progress has been made. Systematic methods can now routinely solve verification problems with thousands or tens of thousanss of variables, whilst local search methods can solve hard random 3SAT problems with millions of variables. In light of this, we are planning another special issue of the Journal of Automated Reasoning, SAT 2005, on the state of the art for research into satisfiability in the year 2005. In addition to the special issue, the accepted papers will be published as a book which will be included as an optional extra in the registration package for the SAT-2005 conference.

Topics

Submission

Timetable

The NWPT series of annual workshops is a forum bringing together programming theorists from the Nordic and Baltic countries (but also elsewhere). The previous workshops were held in Uppsala (1989 and 1999), Aalborg (1990), Gothenburg (1991 and 1995), Bergen (1992 and 2000), Turku (1993, 1998, and 2003), Aarhus (1994), Oslo (1996), Tallinn (1997 and 2002), Lyngby (2001). This time the workshop will be once again held in Uppsala. Typical topics of the workshop include (but are not limited to):

• Semantics of programs
• Programming logics
• Program verification
• Formal specification of programs
• Program synthesis
• Program transformation and program refinement
• Real-Time and hybrid systems
• Modeling of concurrency
• Programming methods
• Tools for program construction and verification

SUBMISSIONS:

PROGRAMME COMMITTEE

IMPORTANT DATES

• September 6 - submission of abstracts
• September 20 - notification of acceptance
• October 6 to 8 - WORKSHOP

MORE INFORMATION