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

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

INTRODUCTION
The second international summer school in Constraint and Logic Programming has been held on the campus of University of Texas at Dallas, TX. The summer school is meant for students, researchers, and programmers interested in constraints, logic programming, computational logic and its applications.
The 2nd summer school on computational logic builds on the highly successful 1st summer school in (C)LP held in Las Cruces, NM, in 1999.

• Constraint Logic Programming and its Applications by Pascal van Hentenryck (Brown University)
• The Semantic Web and Computational Logic by Stefan Decker (Digital Enterprise Research Institute, Ireland)
• Answer Set Programming by Chitta Baral (Arizona State University)
• Tabled Logic Programming and its Applications by David S. Warren (SUNY Stony Brook)
• Logical Aspects of Computer Security by Ninghui Li (Purdue University)
• Inductive Logic Programming and its Applications by Vitor Santos Costa (University of Wisconsin and UFRJ Brazil)
  

• Assume a good heuristic.
• Trust the heuristic less over.
• May avoid being stuck in suboptimal region.
  

• Euler knight: where a knight is required to visit all the positions in the chess-board exactly once.
• Car sequencing: where we need to meet the customers' requirements in assemblying a car (leather seat, sun roof, etc.).
• Scene allocation: this is the problem of producing a movie at minimal cost by deciding when to shoot scenes. Constraints on number of actors, fees and number of scenes per day have to be satisfied.
• Sport scheduling: where n-teams are scheduled to play with each others. Constraints that need to be satisfied include: only two teams are scheduled to play at any time, the period is limited and the number of play for each period is specified.
  

The lectures on Logical Aspects of Computer Security have been offered by Dr. Ninghui Li from Purdue University.

The first lecture took place on June 16, from 4:00 to 6:30. During the first lecture, Dr. Li provided:

• A comprehensive introduction to the fundamental issues of Access Control.
• A brief introduction to Trust Management.
• A discussion of a logic-based semantics for Simple Distributed Security Infrastructure (SDSI).
• A distributed deduction system for Role-based Truth-management languages (RT₀).
  

The second lecture took place on June 17 from 1:00 to 3:30. During this lecture, Dr. Li offered an in-depth of security analysis for
the RT₀ languages. He continued by describing how Constraint Datalog can be used as a semantic foundation for trust-management languages. He concluded his presentation by discussing some open problems in the area of trust-management as well as other possible applications of logic programming in the field of access control.

THE SEMANTIC WEB AND COMPUTATIONAL LOGIC

The lectures on Computational Logic and the Semantic Web have been offered by Dr. Stefan Decker, from the Digital Enterprise Research Institute, Ireland.

The first lecture took place on the first day of the Summer School (June 14) from 9:00 to 11:30. During the first lecture, Dr. Decker provided an overview of what the Semantic Web is, an what are the basic motivations that brought it into existence. Dr. Decker proceeded with an analysis of the information aspects and basic components of the Semantic Web, including a nice discussion of metadata and the Resource Description Framework (RDF).

The second lecture took place on June 15, from 4:00 to 6:30. Dr. Decker  continued his overview of the Semantic Web, focusing in particular on Ontologies. Dr. Decker introduced different formalisms for dealing with ontologies, including Description Logics, the Web Ontology Language (OWL), Description Logic Programming, and F-logic. The discussion proceeded towards applications of logic programming in reasoning about ontologies and current extensions of ontology languages. The lecture closed with a brief picture of the future of the Semantic Web.

TABLED LOGIC PROGRAMMING

The lectures on Tabling in Logic Programming have  been offered by Dr. David S. Warren, from SUNY Stony Brook.

The first lecture took place on June 16, from 9:00 to 11:30. In this lecture, Dr. Warren introduced the problem of non-termination in traditional Prolog systems, through some fundamental examples - such as symmetric and transitive relations.
Dr. Warren continued by showing how these problems can be effectively dealt with using tabled logic programming, and its implementation in the XSB system. The discussion highlighted how tabling can eliminated redundant computation, by storing in a table goals and their previously computed answers. In particular, all programs that do not use structures have been shown to terminate under tabled evaluation.

The second lecture on tabling took place on June 17th, from 4:00 to 6:30. In this lecture, Dr. Warren discussed the following topics:

• Applications of tabled logic programming in Databases, Grammars, Automata Theory and Dynamic Programming.
• A general evaluation strategy for recursive definitions using tabling.
• Program processing using tabling.
• Beyond simple tabling (Negation, Aggregation and Constraints).
  

The lectures on Answer Set Programming have been offered by Dr. Chitta Baral, from Arizona State University.

In the first lecture, Dr. Baral presented the foundations of Knowledge Representation and Reasoning (KRR), and he offered a perspective of how Answer Set Programming - and more specifically its instantiation in the AnsProlog system - can provide a very
effective solution to the key problems of KRR. In his lecture, Dr. Baral presented terminologies, syntax and semantics of AnsProlog. A rich collection of examples have been discussed to introduce AnsProlog, along with a discussion of basic techniques for declarative problem solving using AnsProlog.

During the second lecture, Dr. Baral concentrated on one of the main application of AnsProlog: reasoning about action and planning  Starting from a simple example and its solutions, Dr. Baral led the students to different and more complex problems and how they could be solved effectively using AnsProlog. In the last part, he provided an overview of the current implementations of  systems that can be used to compute answer sets - such as Smodels, DLV, and ASSAT. Dr. Baral closed the lecture with a discussion of the complexity and expressiveness of the AnsProlog* subclass.

INDUCTIVE LOGIC PROGRAMMING

The lectures on Inductive Logic Programming have been offered by Dr. Vitor Santos Costa, from the Federal University of Rio de Janeiro (currently at the University of Wisconsin).

During the first lecture, Dr. Santos Costa gave an overview of the different fields of machine learning and concentrated on Inductive Logic Programming. The presentation of the basic techniques in Inductive Logic Programming developed around the use of the Aleph system and its application to solve Michalski's train problem.
Dr. Santos Costa showed how the system can be used to tackle this example, and some specific techniques that have been applied in the implementation of Aleph. The discussion continued with a description of the structure of the search space in inductive logic programming and how its efficient exploration is tackled in the existing systems.
The lecture closed with the analysis of the issues of correctness and with the presentation of another system, FOIL, to discuss other inductive logic programming techniques.

During the second lecture, Dr. Santos Costa started with the principles of Inductive Logic Programming. The techniques introduced in the first lecture have been revisited in detail and in the context of both top-down and bottom-up approaches. Dr. Santos Costa introduced the principles of least generalization and refinement, and their use in some popular systems (e.g., GOLEM).
Dr. Santos Costa closed his presentation with some examples of applications of inductive logic programming,  and with an overview  of the main current research efforts in this field.

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

Knowledge Representation Group at TTU

The Knowledge Representation Group at Texas Tech University (Lubbock, Texas) was created in the year 2000 and initially consisted of two faculty members, Michael Gelfond and Richard Watson, two graduate students Marcello Balduccini and Veena Mellarkod who moved to TTU from El Paso, and two other students Monica Nogueira and Mary Lynn Heidt, who stayed in El Paso. Monica and Mary successfully graduated, and later we were joined by six new student members including two PhD students. Our work is centered around two research themes:

1. Declarative Languages for Knowledge Representation.
2. Design and Implementation of Intelligent Agents.

Declarative Languages for Knowledge Representation

(a) ASET -- the language which allows use of sets and aggregates in the body of a rule as well as expressions of the form ``Let p be a subset of {X:q(X)}'' in a rule head. The latter is similar but not equivalent to the choice rule of Smodels.

(b) CR-Prolog -- the language that extends ASET by allowing consistency restoring rules of the form

1.
2. .
3. .

The programs consisting of rules (1) and (1,2) have the same answer set, {p}, while the program consisting of rules (1,2,3) has the answer set . The language, expanded by a notion of "binding" preference between consistency restoring rules, allows to nicely combine deductive and abductive reasoning.

(c) P-log -- an extension of Answer Set Prolog which allows one to combine probabilistic and logical reasoning. The language, inspired by Judea Pearl's work on causality, allows one to accurately formalize subtle probabilistic and causal arguments.

The latter includes development of action languages for non-markovian domains, domains with continuous processes, non-deterministic actions, etc.

Currently we are working on the methodology of using these languages for knowledge representation, development and implementation of the corresponding reasoning algorithms, and investigation of the relationship between these and other similar extensions of Answer Set Prolog.

Design and Implementation of Intelligent Agents

Our future plans include the search for a simple and mathematically precise architecture of an agent capable of combining these and other reasoning tasks with constant monitoring of an environment and a built-in reactive behavior. We also plan to better understand properties of P-log, learn to perform counterfactual reasoning, and investigate how our reasoning methods can be integrated with natural language processing.

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

http://www.krlab.cs.ttu.edu/.

1. INTRODUCTION

In this article we describe the SOCS project. SOCS is concerned with a computational logic model for the description, analysis and verification of global and open SOcieties of heterogeneous ComputeeS, where computees are computational entities, that is agents realised in computational logic. SOCS is funded by the European Commission under the Fifth Framework, Future and Emerging Technologies programme, within the Global Computing proactive initiative. The SOCS consortium is composed of six European partners, based in Italy, UK, and Cyprus. These are, respectively, the universities of Pisa, Bologna and Ferrara (Italy), Imperial College and City University (UK), and Cyprus University. The project is coordinated by Imperial College.
The project started in January 2002 and will finish in June 2005. Its aims are

Details of the project can be found at the project web-site:

Article overview. The remainder of this article is structured as follows. Sections 2 and 3 provide an overview of the models developed for individual computees and for societies of computees, respectively. Section 4 summarises the prototype implementations, and Section 5 concludes.

2. COMPUTEES

• an internal (or mental) state,
• a set of reasoning capabilities, supporting planning, temporal reasoning, identification of preconditions of actions, reactivity and goal decision,
• a sensing capability,
• a set of transition rules, defined in terms of the above capabilities, and describing how the state of the computee changes,
• a set of selection functions, to provide appropriate inputs to the transitions, and
• a cycle theory, for deciding which transitions should be applied when, and defined using the selection functions.
  

• KB is the knowledge base of the computee, and describes what the computee knows (or believes) of itself and the environment. KB consists of modules supporting different reasoning capabilities:
• KB_plan, for Planning,
• KB_pre, for the Identification of Preconditions of actions,
• KB_TR, for Temporal Reasoning,
• KB_GD, for Goal Decision,
• KB_react, for Reactivity, and
• KB₀, for holding the (dynamic) knowledge of the computee about the external world in which it is situated (including past communications).
  

• Goals is the set of properties that the computee wants to achieve, each one explicitly time-stamped by a time variable. Goals may also be equipped with a temporal constraint (belonging to TCS, described later) constraining the time variable. Goals may be mental or sensing. Both can be observed to hold (or not to hold) via the Sensing capability. In addition, mental goals can be brought about actively by the computee by its Planning capability and its actions.
• Plan is a set of actions scheduled in order to satisfy goals. Each action is explicitly time-stamped by a time variable and possibly equipped with a temporal constraint, similarly to Goals, but defining when the action should be executed. Actions are partially ordered, via their temporal constraints. Each action is also equipped with the preconditions for its successful execution, determined by the Identification of Preconditions capability. Actions may be physical, communicative, or sensing. We assume that actions are atomic and do not have a duration. Actions can be seen as special kinds of goals which are directly executable.
• TCS is a set of constraint atoms (referred to as temporal constraints) in some given underlying constraint language with respect to some structure equipped with a notion of constraint satisfaction . We assume that the constraint predicates include <, >, , , = , . Temporal constraints refer to time constants, namely natural numbers, and time variables, namely distinguished variables which can be instantiated to time constants. These constraints restrict the time of goals in Goals and actions in Plan.

• Planning, which generates partial plans for sets of goals. It provides (temporally constrained) sub-goals and actions designed for achieving the input goals.
• Reactivity, which reacts to perceived changes in the environment, by adding goals in Goals and actions in Plan (with appropriate temporal constraints).
• Goal Decision, which revises the top-most level goals of the computee, adapting the computee’s state to changes in its own preferences and in the environment. Differently from Reactivity, it only modifies the top-level goals. It does not add actions to Plan and it does not depend upon the current Goals and Plan.
• Identification of Preconditions, which identifies the preconditions for action execution.
• Temporal Reasoning, which reasons about the environment, and makes predictions about properties holding in the environment, based on the partial information the computee acquires.
  

• Goal Introduction (GI), changing the top-level Goals, and using Goal Decision.
• Plan Introduction (PI), changing Goals and Plan, and using Planning and Introduction of Preconditions.
• Reactivity (RE), changing Goals and Plan, and using the Reactivity capability.
• Sensing Introduction (SI), changing Plan by introducing new sensing actions for checking the preconditions of actions already in Plan, and using Sensing.
• Passive Observation Introduction (POI), changing KB₀ of KB by introducing unsolicited information coming from the environment, and using Sensing.
• Active Observation Introduction (AOI), changing KB₀ of KB, by introducing the outcome of (actively sought) sensing actions, and using Sensing.
• Action Execution (AE), executing all types of actions, and changing KB₀ of KB by recording their execution.
• Goal Revision (GR), revising Goals, and using Temporal Reasoning and Constraint Satisfaction. GR removes those goals that are achieved, timed-out or have become unnecessary.
• Plan Revision (PR), revising Plan and using Constraint Satisfaction. PR removes those actions that are either timed-out or that have become unnecessary.

• the CIFF proof procedure for abductive logic programming [8, 9], which is an extension of the IFF proof procedure of [10] to deal with constraint predicates and non-allowed abductive logic programming;
• GORGIAS [7], a novel system for logic programming with priorities based upon an existing proof theory for computing admissible arguments for abstract argumentation frameworks [14].
  

3. SOCIETY OF COMPUTEES

4. PROTOTYPE IMPLEMENTATION

Figure 1: The conceptual organization of PROSOCS

To facilitate experimentation with KGP agents we have built interfaces, which allow us to animate an agent’s behaviour while interacting with other agents in the context of a Global Computing application. The aspects of the agent’s behaviour that we animate, in the current state of the implementation, are: the computational trace in terms of the names of transitions being executed, the observations the agent makes and the actions it executes, the internal state of the agent in terms of its knowledge, goals and plans. More details of the implementation of the agent template can be found in [17].

SOCSiC is complemented by SOCS-SI which implements the Society Infrastructure (see Figure 3) of PROSOCS, and it is committed to the verification of compliance to protocols of the computees’ interactions.

The verification is performed by means of the SCIFF abductive proof procedure (see [6]).

As summarised in Section 3, the knowledge about the interaction protocols in the society is represented by an abductive logic program (composed of a logic program called knowledge base, a set of Social Integrity Constraints and a set of abducibles), while the knowledge about the agent interaction is represented as a history of events. Given a (partial) history of the agent interaction, SCIFF generates a set of abducibles (expectations) which represent a course of action that would satisfy the interaction protocols; checking the expectations against the events, the society module is able to determine fulfillment (the interaction protocols have been respected) or violation (the interaction protocols have not been respected).

The SCIFF proof procedure is implemented in SICStus Prolog [15]; the SOCS-SI GUI is implemented in Java.

Figure 2: Implementation architecture of PROSOCS computee (SOCS-iC)

5. CONCLUSION

Figure 3: Overview of the society infrastructure architecture (SOCS-SI)

REFERENCES

• Images from ICLP 2003
  
• European Master on Language and Communication Technologies
  
• New Journal: Logical Methods in Computer Science
• International Master in Computational Logic
• 10th Prolog Programming Contest
  

• Curriculum taught entirely in English: The programme is open to the world and prepares the students to move on the international scene.
• Possibility of a strongly research-oriented curriculum. 
• Possibility for project-based routes to obtain the degree and extensive lab facilities. 
• Other specialisations with streams in the hottest Computer Science areas, such as Web Technologies, Information and Knowledge Management, Databases and Software Engineering. 
• International student community. 
• Direct interaction with the local and international industry and research centres, with the possibility of practical and research internships that can lead to future employment. 
• Excellent scholarship opportunities and student accommodations.
  

• State of the art computing infrastructure
• Computer lab with facilities for the visually impaired 
• Eye-tracking lab 
• Speech labs 
• Dialogue and usability lab 
• Video conferencing lab 
• In-house Institute library
  

• Being Or Not (Any Longer) Being Open-Source
• Portability Again
• Views on the History of Prolog Standardization
• The Sad Truth
  

Andrzej Lewandowski wrote:
> Or, I don't undserstand the term "open source"...

I think you do.
I lost interest in B-Prolog the day I (and others) had to pay for sources. Same for BinProlog.
It's such a shame - those systems that move from academic to commercial.

As gcc and other open source products show, their "open sourceness" is not in conflict with commercial success. I am using Prolog in commercial environment where we have nothing against using open source products, but we always purchase maintenance contracts and commercial licenses.

I was considering using B-Prolog, but despite positive technical evaluations it was rejected for business reasons. It would be unwise for us to use a product developed by single-person academic spinoff as a foundation of costly project. Situation would be different with open source product with solid maintenance and support. The likelihood that open source product gets extinct is substantially less than for product developed by in-my-basement company.

Pity that authors  of academic-gets-commercial stuff don't recognize open source movement as an opportunity....

OOskar Bartenstein wrote:
> Interesting opinion.
> Can you (or anybody else) explain what is so bad about this pattern?

You forgot an important part of what I wrote:

 >> I lost interest in [...] the day I (and others) had to pay for
 >> sources.

It's about systems that used to be free as a subject for research (which means to me "sources"), and now money is involved; or worse: one can't get the sources at all (unless by joining the company).
I don't mind people moving from academic to commercial, I don't even mind commercial people making a living thanks to academics; what I don't like is commercial people hiding things from, or putting up barriers for academics. Especially when the bariers weren't there before.
But it is a free world.

[...]

Christoph Quix wrote:
> And for the future, what is the best way to maintain
> a project that should be portable between different
> Prolog compilers? I am thinking of something like
> a preprocessor for Prolog (enabling #ifdef and similar
> things in Prolog).

Its a difficult issue. For nice and clean Prolog code, stick with ISO builtins and you should be fairly portable. You want modules (I guess). SICStus, CIAO, SWI and YAP (also GNU?) are very similar.  Libraries is a big issue.  All systems have different libraries containing different predicates.  Term-expansion and/or goal expansion are an option.  So is using an external preprocessor such as cpp, thouch cpp can easily be fooled by Prolog syntax (think of 0'a) and it doesn't make the development cycle easier (SWI-Prolog has an option to define an external preprocessor, though it is used very rarely).

GNU Prolog does not have a module system. The same goes for a number of Prolog compilers. Some potential portability pitfalls when using current module systems are meta-predicates and operators. The module systems of Quintus/SICStus use a meta_predicate directive for declaring meta-predicates. SWI-Prolog uses a module_transparent directive. At least one of the module systems for the Prolog compilers cited above does not support local operators inside modules (operators declared within modules have global scope). There is no formal (or semi-formal) specification (to the best of my knowledge; please correct me if I'm wrong) for the module system used by the Prolog compilers cited above. The Part II of the ISO Prolog standard specifies a module system which is incompatible with most module systems in use today (which, btw, pre-dates the ISO standard!!!). One of the highlights of the ISO standard is to leave to the Prolog implementer a choice between two incompatible ways of dealing with meta-predicates. I'm belief there might be valid reasons to use (today) module systems within the context of a specific Prolog compiler. Portability between a wide range of Prolog compilers is certainly not one of them.

• 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
  
  
• A uniform approach to logic programming semantics. [CoRR]
  Pascal Hitzler and Matthias Wendt

• Abductive Logic Programs with Penalization: Semantics, Complexity and Implementation. [CoRR]
  Simona Perri, Francesco Scarcello and Nicola Leone

• Inferring Termination Conditions for Logic Programs using Backwards Analysis. [CoRR]
  Samir Genaim and Michael Codish

• A Parameterised Hierarchy of Argumentation Semantics for Extended Logic Programming and its Application to the Well-founded Semantics. [CoRR]
  Ralf Schweimeier and Michael Schroeder

SPECIAL ISSUE on Verification and Computational Logic

• Introduction to the Special Issue on Verification and Computational Logic,
  Michael Leuschel, Andreas Podelski, C.R. Ramakrishnan, Ulrich Ultes-Nitsche

• On model checking data-independent systems with arrays without reset,
  R.S. Lazi\'c, T.C. Newcomb, A.W. Roscoe,

• Inference of termination conditions for numerical loops in Prolog,
  Alexander Serebrenik and Danny De Schreye, [CoRR]

• Model Checking Linear Logic Specifications,
  Marco Bozzano, Giorgio Delzanno, Maurizio Martelli, [CoRR]

• Temporalized logics and automata for time granularity,
  Massimo Franceschet and Angelo Montanari, [CoRR]

• Ackermann Encoding, Bisimulations, and OBDDs,
  Carla Piazza and Alberto Policriti, [CoRR]

• Soft Constraint Programming to Analysing Security Protocols,
  Giampaolo Bella and Stefano Bistarelli, [CoRR]

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
• Monodic temporal resolution Anatoly Degtyarev, Michael Fisher and Boris Konev
• An Elementary Fragment of Second-Order Lambda Calculus K. Aehlig and J. Johannsen
• Heterogeneous Temporal Probabilistic Agents Juergen Dix, Sarit Kraus and VS Subrahmanian
• Constant-Depth Frege Systems with Counting Axioms Polynomially Simulate Nullstellensatz Refutations Russell Impagliazzo and Nathan Segerlind
• Optimizing Optimal Reduction: A Type Inference Algorithm for Elementary Affine Logic Paolo Coppola and Simone Martini
• Why Are There So Many Loop Formulas? Vladimir Lifschitz and Alexander Razborov
• Decidability Results for Sets with Atoms Agostino Dovier, Andrea Formisano and Eugenio Omodeo
• Propositional computability logic I Giorgi Japaridze
• Ordinary Interactive Small-Step Algorithms, I Andreas Blass and Yuri Gurevich
• Logic Program Based Updates Yan Zhang

Multi-agent systems are communities of problem-solving entities that can perceive and act upon their environments to achieve their individual goals as well as joint goals. the work on such systems integrates many technologies and concepts in artificial intelligence and other areas of computing. for this reason, over recent years, the agent paradigm gained popularity in many sub-fields of computer science. a full spectrum of multi-agent systems applications have been and are being developed; from search engines to educational aids to electronic commerce and trade, e-procurement, recommendation systems, simulation and routing, to cite only some.

Although commonly implemented by means of imperative languages, mainly for reasons of efficiency, the agent concept has recently increased its influence in the research and development of computational logic based systems.

Computational logic provides a well-defined, general, and rigorous framework for studying syntax, semantics and procedures, for attending implementations, environments, tools, and standards, and for linking together specification and verification of properties of computational systems.

The purpose of this workshop is to discuss techniques, based on computational logic, for representing, programming and reasoning about multi-agent systems in a formal way.

• a computational model for conversation policies for agent communication
  jamal bentahar, bernard moulin, john-jules ch. meyer, brahim chaib-draa

• an application of global abduction to an information agent which modifies a plan upon failure - preliminary report -
  ken satoh

• coordination between logical agents
  chiaki sakama, katsumi inoue

• organising software in active environments
  michael fisher, benjamin hirsch, chiara ghidini, paolo busetta

• planning partially for situated agents
  paolo mancarella, fariba sadri, giacomo terreni, francesca toni

• contextual taxonomies
  davide grossi, frank dignum, john-jules meyer

• dynamic logic for plan revision in intelligent agents
  m. birna van riemsdijk, frank s. de boer, john-jules ch. meyer

• graded bdi models for agent architectures.
  ana casali, lluís godo, carles sierra

• verifying protocol conformance for logic-based communicating agents
  matteo baldoni, cristina baroglio, alberto martelli, viviana patti, claudio schifanella

• solving collaborative fuzzy agents problems with clp(fd)
  susana muñoz hernández, jose manuel gómez pérez

• inferring trust
  mehdi dastani, andreas herzig, joris hulstijn, leendert van der torre

• declarative agent control
  antonis kakas, paolo mancarella, fariba sadri, kostas stathis, francesca toni

• metareasoning for multi-agent epistemic logics
  konstantine arkoudas, selmer bringsjord

• desire-space analysis and action selection for multiple dynamic goals
  david c. han, k. suzanne barber

• dynamic logic programming: various semantics are equal on acyclic programs
  martin homola

• from logic programs updates to action description updates
  josé julio alferes, federico banti, antonio brogi

ACCEPTED PAPERS:

• Two Approaches to Merging Knowledge Bases, James P. Delgrande, Torsten Schaub
• Line-based affine reasoning in Euclidean plane, Philippe Balbiani, Tinko Tinchev
• Representation and Complexity in Boolean Games, Paul E. Dunne, Wiebe van der Hoek
• Negative Hyper-Resolution as Procedural Semantics of Disjunctive Logic Programs, Linh Anh Nguyen
• Explaining Subsumption by Optimal Interpolation, Stefan Schlobach
• Combining Decision Procedures for Sorted Theories, Cesare Tinelli, Calogero G. Zarba
• Transforming Fuzzy Description Logics into Classical Description Logics, Umberto Straccia
• Complexity in Value-Based Argument Systems, Paul E. Dunne, Trevor Bench-Capon
• Reasoning about Quantum Systems, P. Mateus, A. Sernadas
• Towards a First Order Equilibrium Logic for Nonmonotonic Reasoning, David Pearce, Agustin Valverde
• A Polynomial Translation of the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment, Yevgeny Kazakov
• Soundness and Completeness of an "Efficient" Negation for Prolog, Juan José Moreno Navarro, Susana Muñoz Hernández
• An Algebraic Approach to Belief Contraction and Nonmonotonic Entailment, Lee Flax
• Polynomial Approximations of Full Propositional Logic via Limited Bivalence, Marcelo Finger
• Games for Cognitive Agents, Mehdi Dastani, Leendert van der Torre
• A logic for reasoning about coherent conditional probability: a modal fuzzy logic approach, Lluis Godo, Enrico Marchioni
• Hierarchical Decision Making by Autonomous Agents, Stijn Heymans, Davy Van Nieuwenborgh, Dirk Vermeir
• Logic Programs with Functions and Default Values, Pedro Cabalar, David Lorenzo
• Exploiting functional dependencies in declarative problem specifications, Marco Cadoli, Toni Mancini
• Knowledge-theoretic properties of strategic voting, Samir Chopra, Eric Pacuit, Rohit Parikh
• Meta-level Verification of the Quality of Medical Guidelines using Interactive Theorem Proving, Arjen Hommersom, Peter Lucas, Michael Balser
• Towards a Logical Analysis of Biochemical Pathways, Patrick Doherty, Steve Kertes, Martin Magnusson, Andrzej Szalas
• Discovering Anomalies in Evidential Knowledge by Logic Programming, Fabrizio Angiulli, Gianluigi Greco, Luigi Palopoli
• TimeGranularities and Ultimately Periodic Automata, Davide Bresolin, Angelo Montanari, Gabriele Puppis
• Measure Logics for Spatial Reasoning, Mehmet Giritli
• Parallel Encodings of Classical Planning as Satisfiability, Jussi Rintanen, Keijo Heljanko, Ilkka Niemelä
• Equivalence of Logic Programs under Updates, Katsumi Inoue, Chiaki Sakama
• On sceptical vs credulous acceptance for abstract argument systems, Sylvie Doutre, Jerome Mengin
• Characterizations for Relativized Notions of Equivalence in Answer Set Programming, Stefan Woltran
• Verifying Communicating Agents by Model Checking in a Temporal Action Logic, Laura Giordano, Alberto Martelli, Camilla Schwind
• An Answer Set Programming of Prioritized Removed Sets Revision: Application to GIS, Bennaim Jonathan, Benferhat Salem, Papini Odile, Wurbel Eric
• The Modal Logic Programming System MProlog, Linh Anh Nguyen
• A Logic with Conditional Probabilities, Miodrag Raskoviæ, Zoran Ognjanoviæ, Zoran Markoviæ
• Branch-Saturation in Free-Variable Tableaux, Nicolas Peltier
• Computing the Least Common Subsumer w.r.t. a Background Terminology, Franz Baader, Baris Sertkaya, Anni-Yasmin Turhan
• Only Knowing: Reductions and Complexity, Espen Hallenstvedt Lian, Arild Waaler, Tore Langholm
• The CIFF Proof Procedure for Abductive Logic Programming with Constraints, Ulle Endriss, Paolo Mancarella, Fariba Sadri, Giacomo Terreni, Francesca Toni
• Logic Programming Infrastructure for Inferences on FrameNet, Peter Baumgartner, Aljoscha Burchardt
• Practical Reasoning for Uncertain Agents, Nivea de Carvalho Ferreira, Michael Fisher, Wiebe van der Hoek
• Relational Markov Games, Alberto Finzi, Thomas Lukasiewicz
• An Implementation of Statistical Default Logic, Gregory R. Wheeler, Carlos Damásio
• Epistemic logic for rule-based agents, Natasha Alechina, Brian Logan, Mark Whitsey
• Capturing Parallel Circumscription with Disjunctive Logic Programs, Tomi Janhunen, Emilia Oikarinen
• Cardinality Constraint Programs, Tommi Syrjänen
• Semantic Knowledge Partitioning, Christoph Wernhard
• Sorted multi-adjoint logic programs: termination results with applications, Carlos V. Damásio, Jesus Medina, Manuel Ojeda-Aciego
• On the relation between ID-Logic and Answer Set Programming, David Gilis, Maarten Mariën, Marc Denecker
• Alternating-Time Temporal Logic and the Kutschera-Belnap Approach to Agency, Stefan Wölfl
• Logical connectives for nonmonotonicity: A choice function-based approach, Jérôme Mengin
• Recursive Aggregates in Disjunctive Logic Programs: Semantics and Complexity, Wolfgang Faber, Nicola Leone, Gerald Pfeifer
• A logical analysis of temporally constrained motivational attitudes, Jan Broersen
• Automatic Compilation of Protocol Insecurity Problems into Logic Programming, Alessandro Armando, Yuliya Lierler, Luca Compagna

ACCEPTED SYSTEM DEMONSTRATIONS:

• Abductive Logic Programming with CIFF: System Description, U. Endriss, P. Mancarella, F. Sadri, G. Terreni and F. Toni
• The DALI Logic Programming Agent-Oriented Language, S. Costantini and A. Tocchio 
• Qsmodels: ASP Planning in Interactive Gaming Environment, L. Padovani and A. Provetti 
• A system with template answer set programs, F. Calimeri, G. Ianni, G. Ielpa, A. Pietramala and M. C. Santoro 
• New DLV Features for Data Integration, F. Calimeri, M. Citrigno, C. Cumbo, W. Faber, N. Leone, S. Perri and G. Pfeifer 
• Profiling Answer Set Programming: The Visualization Component of the noMoRe System, A. Bösel, T. Linke and T. Schaub 
• The PLP System, T. Wakaki, K. Inoue, C. Sakama and K. Nitta 
• The MyYapDB Deductive Database System, M. Ferreira and R. Rocha 
• InterProlog: towards a declarative embedding of logic programming in Java, M. Calejo 
• IndLog - Induction in Logc, R. Camacho 
• OLEX - A reasoning-based text classifier, C. Cumbo, S. Iiritano and P. Rullo 
• Verdi: an Automated Tool for Web Sites Verification, M. Alpuente, D. Ballis and M. Falaschi 
• SATMC: a SAT-based Model Checker for Security Protocols, A. Armando and L. Compagna 
• tabeql: a tableau based suite for Equilibrium Logic, A. Valverde 
• tascpl: TAS solver for Classical Propositional Logic, M. Ojeda-Aciego and A. Valverde
  

The aim of the LOPSTR  series is to stimulate and promote international research and collaboration on logic-based program development, and the workshop is open to contributions in logic-based program development in any language paradigm.

LOPSTR'04 will be held at the University of Verona http://www.univr.it co-located with SAS 2004 http://www.sci.univr.it/~sas04 the International Static Analysis Symposium, PEPM 2004 http://www.sci.univr.it/~pepm04 - ACM SIGPLAN 2004 Workshop on Partial Evaluation and Semantics Based Program Manipulation, and PPDP 2004 http://www.sci.univr.it/~ppdp04 - 6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming.

Past workshops were held in Manchester, UK (1991, 1992, 1998), Louvain-la-Neuve, Belgium (1993), Pisa, Italy (1994), Arnhem, the Netherlands (1995), Stockholm, Sweden (1996), Leuven, Belgium (1997), Venice, Italy (1999), London, UK (2000), Paphos, Cyprus (2001), Madrid, Spain (2002), Uppsala, Sweden (2003). Since 1994 the proceedings have been published in the LNCS series of Springer-Verlag.

LOPSTR also aims to be a lively, friendly forum for presenting and discussing work in progress, so it is a real workshop in the sense that it is also intended to provide useful feedback to authors on their preliminary research. Formal proceedings of the workshop are produced only after the workshop, so that authors can incorporate this feedback in the published papers.

Accepted Papers:

• Searching Semantically Equivalent Code Fragments in Logic Programs      [#14]
  Wim Vanhoof
• Determinacy Analysis for Logic Programs Using Mode and Type Information.   [#22]
  Pedro Lopez-Garcia, Francisco Bueno and Manuel Hermenegildo
• Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs      [#20]
  Sandeep S. Kulkarni, Borzoo Bonakdarpour, Ali Ebnenasir
• Fully Automatic Binding Time Analysis for Prolog      [#ex 3]
  Stephen-John Craig, John P. Gallagher, Michael Leuschel and Kim S. Henriksen
• Logical Mobility and Locality Types    [#18]
  Jonathan Moody
• An Unwinding Condition for Security in Imperative Languages    [#ex 5]
  Annalisa Bossi, Carla Piazza, Sabina Rossi
• Natural rewriting and narrowing for general term rewriting systems     [#ex 9]
  Santiago Escobar, José Meseguer, and Prasanna Thati
• Negation Elimination for Finite PCFGs    [#2]
  Taisuke Sato, Yoshitaka Kameya
  Specialization of Concurrent Guarded Multi-Set Transformation Rules    [#16]
  Thom Fruehwirth
• Efficient Leftmost Unfolding with Ancestor Stacks    [#ex 8]
  German Puebla and Elvira Albert
• Schema-Guided Synthesis of Imperative Programs by Constraint Solving   [#19]
  Michael A. Colon
• Run-Time Profiling of Functional Logic Programms    [#ex 7]
  B.Brassel M. Hanus F. Huch J. Silva G. Vidal
• Constructive Specifications for Compositional Units     [#ex 12]
  Kung-Kiu Lau, Alberto Momigliano, and Mario Ornaghi
• Input-termination of logic programs     [#4]
  M. R. K. Krishna Rao
• On termination of binary CLP programs     [#9]
  Alexander Serebrenik and Fred Mesnard
• Inferring Polymorphic Types from Logic Programs    [#ex 2]
  Maurice Bruynooghe and John Gallagher
• From Natural Semantics to Abstract Machines     [#10]
  Mads Sig Ager
• Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis    [#7]
  J. B. Wells and Boris Yakobowski
• An Approach to Transformational Development in Logical Frameworks    [#ex 4]
  Maksym Bortin Einar Broch Johnsen Christoph Lüth

Workshop Program:

Preliminary Program:

Monday, September 6th
WLPE session, 14:30-16:30

• 14:30-15:30: Invited Talk. Regular types, modes and model checking
  John Gallagher

• 15:30-16:00: On termination of binary CLP programs
  Alexander Serebrenik and Fred Mesnard

• 16:00-16:30: Upsh: A Unix to Prolog Shell
  Nicos Angelopoulos

Tuesday, September 7th
MultiCPL session, 11:00 - 12:30

• 11:00-11:30: Assumptions and Abduction in Prolog
  Henning Christiansen and Veronica Dahl

• 11:30-12:00: Strategies for the Efficient Solution of Hybrid Constraint Logic Programs
  Stephan Frank, Petra Hofstedt, and Dirk Reckmann

• 12:00-12:30: Towards Temporal Reasoning in Constraint Contextual Logic Programming
  Vitor Beires Nogueira, Salvador Abreu, and Gabriel David
  

WLPE session, 14:30 - 17:00

• 14:30-15:30: Invited talk. Prolog Models for the Model-View-Controller Paradigm
  David S. Warren

• 15:30-16:00: A Logic Programming-based Environment for Integrating Architecture Description Languages
  Qian Wang and Gopal Gupta

• 16:00-16:30: FDBG, the CLP(FD) Debugger Library of SICStus Prolog
  Dávid Hanák and Tamás Szeredi

• 16:30-17:00: Explanations to Understand the Trace of a Finite Domain Constraint Solver
  Gérard Ferrand, Willy Lesaint, and Alexandre Tessier

Accepted Papers:

•  On Subtyping of Tree-structured Data A Polynomial Approach
  François Bry, Wlodzimierz Drabent, and Jan Maluszynski 
  
• Towards generic query, update, and event languages for the Semantic Web
  Wolfgang May, José Júlio Alferes, and François Bry 
• Data Retrieval and Evolution on the (Semantic) Web: A Deductive Approach
François Bry, Tim Furche, Paula-Lavinia Patrânjan, and Sebastian Schaffert

• Rules and Queries with Ontologies: a Unified Logical Framework
  Enrico Franconi and Sergio Tessaris 
• Semantic Web Reasoning for Ontology-based Integration of Resources
  Liviu Badea, Doina Tilivea, Anca Hotaran 
• Static Typechecking of Datalog with Ontologies
  Jakob Henriksson and Jan Maluszynski 
• Reasoning about Temporal Context using Ontology and Abductive Constraint Logic Programming
  Hongwei Zhu, Stuart E. Madnick, and Michael D. Siegel 
• Towards a Multi-Calendar Temporal Type System for (Semantic) Web Query Languages
  François Bry and Stephanie Spranger 
• Calendrical Calculations with Time Partitionings and Fuzzy Time Intervals
  Hans Jürgen Ohlbach 
• DR-DEVICE: A Defeasible Logic System for the Semantic Web
  Nick Bassiliades, Grigoris Antoniou, and Ioannis Vlahavas 
• A PDDL based Tool for Automatic Web Service Composition
  Joachim Peer
  

Monday, September 20

Session 1: 9.00 am – 10.15 am

Invited talk: Ken McMillan, Applications of Craig Interpolation to Model Checking

Session 2: 10.45 am – 12.15 pm

Krishnendu Chatterjee, Rupak Majumdar, and Marcin Jurdzinski, On Nash Equilibria in Stochastic Games

Mikolaj Bojanczyk, A Bounding Quantifier

Hugo Gimbert, Parity and Exploration Games on Infinite Graphs

Session 3: 1.30 pm – 3.00 pm

Harald Ganzinger and Konstantin Korovin, Integrating Equational Reasoning into Instantiation-based Theorem Proving

George Metcalfe, Nicola Olivetti, and Dov Gabbay, Goal-Directed Methods for Lukasiewicz Logic

Jeremy E. Dawson and Rajeev Goré, A General Theorem on Termination of Rewriting

Session 4: 3.30 pm – 5.00 pm

Pierre Hyvernat, Predicate Transformers and Linear Logic: yet another Denotational Model

Pietro Di Gianantonio, Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity

Lutz Straßburger and François Lamarche, On Proof Nets for Multiplicative Linear Logic with Units

Tuesday, September 21

Session 5: 9.00 am – 10.15 am

Invited talk: Pawel Urzyczyn, My (Un)Favourite Things

Session 6: 10.45 am – 12.15 pm

Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv and Greta Yorsh, The Boundary Between Decidability and Undecidability for Transitive Closure Logics

Marcelo Arenas, Pablo Barceló, and Leonid Libkin, Game-based Notions of Locality over Finite Models

Andreas Abel and Ralph Matthes, Fixed Points of Type Constructors and Primitive Recursion

Session 7: 1.30 pm – 3.00 pm

Aleksy Schubert, On the Building of Affine Retractions

Philippe de Groote and Sylvain Salvati, Higher-order Matching in the Linear λ-calculus with Pairing

Ulrich Schöpp and Ian Stark, A Dependent Type Theory with Names and Binding

Session 8: 3.30 pm – 5.00 pm

Tjark Weber, Towards Mechanized Program Verification with Separation Logic

Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, and Line Jakubiec, A Functional Scenario for Bytecode Verification of Resource Bounds

Roberto Giacobazzi and Isabella Mastroeni, Proving Abstract Non-Interference

Wednesday, September 22

Session 9: 9.00 am – 10.15 am

Invited talk: Dale Miller, Bindings, mobility of bindings, and the ∇-quantifier

Session 10: 10.45 am – 12.15 pm

Patrick Maier, Intuitionistic LTL and a New Characterization of Safety and Liveness

Philipp Rohde, Moving in a Crumbling Network: The Balanced Case

E. Allen Emerson and Vineet Kahlon, Parameterized Model Checking of Ring-based Message Passing Systems

Thursday, September 23

Session 11: 9.00 am – 10.15 am

Invited talk: Martin Hyland, Abstract Interpretation of Proofs: Classical Propositional Logic

Session 12: 10.45 am – 12.15 pm

Alan Skelley, A Third-Order Bounded Arithmetic Theory for PSPACE

Andrés Cordón-Franco, Alejandro Fernández-Margarit, and F. Félix Lara-Martín, Provably Total Primitive Recursive Functions: Theories with Induction

David Richerby, Logical Characterizations of PSPACE

Session 13: 1.30 pm – 3.00 pm

Lutz Schröder, The Logic of the Partial λ-Calculus With Equality

Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, and Yu Zhang, Complete Lax Logical Relations for Cryptographic Lambda-Calculi

Jérôme Vouillon, Subtyping Union Types

Session 14: 3.30 pm – 5.00 pm

Margarita Korovina and Nicolai Vorobjov, Pfaffian Hybrid Systems

Yukiyoshi Kameyama, Axioms for Delimited Continuations in the CPS Hierarchy

Pawel Rychlikowski and Tomasz Truderung, Set Constraints on Regular Terms

Friday, September 24

Session 15: 9.00 am – 10.15 am

Invited talk: Albert Atserias, Notions of Average-Case Complexity for Random 3-SAT

Session 16: 10.45 am – 12.15 pm

Christopher Lynch, Unsound Theorem Proving

Alessandro Avellone, Camillo Fiorentini, Guido Fiorino, and Ugo Moscato, An Efficent Implementation of a Tableau Calculus for a Logic with a Constructive Negation

Agata Ciabattoni, Automated Generation of Analytic Calculi for Logics with Linearity

Distinguished Papers:
Paper 26: Consistency and Random Constraint Satisfaction Models with a high Constraint Tightness
Yong Gao and Joseph Culberson

Paper 68: Constraint-Based Combinators for Local Search
Pascal Van Hentenryck, Laurent Michel, and Liyuan Liu

Paper 86: Unary Resource Constraint with Optional Activities
Petr Vilim, Roman Bartak, Ondrej Cepek

Paper 176: Statistical Regimes Across Constrainedness Regions
Carla Gomes, Cesar Fernandez, Bart Selman, and Christian Bessiere

Full Papers:

Paper 9: Theoretical Foundations of CP-based Lagrangian Relaxation
Meinolf Sellmann

Paper 13: Set Domain Propagation Using ROBDDs
Vitaly Lagoon and Peter J. Stuckey

Paper 25: Heuristic Selection for Stochastic Search Optimization: Modeling Solution Quality by Extreme Value Theory
Vincent A. Cicirello, Stephen F. Smith

Paper 32: A hybrid method for planning and scheduling
John Hooker

Paper 49: Deriving Filtering Algorithms from Constraint Checker
Nicolas Beldiceanu, Mats Carlsson, Thierry Petit

Paper 56: Constraint Satisfaction in Semi-structured Data Graphs
Nikos Mamoulis, Kostas Stergiou

Paper 60: Decomposition and learning for a real time task allocation problem
Hadrien Cambazard, Pierre-Emmanuel Hladik, Anne-Marie Diplanche, Narendra Jussien, Yvon Trinquet
 

Paper 67: Leveraging the Learning Power of Examples in Automated Constraint Acquisition
Christian Bessiere, Remi Coletta, Eugene C. Freuder, and Barry O'Sullivan

Paper 72: Disjoint, Partition and Intersection Constraints for Set and Multiset Variables
Christian Bessiere, Emmanuel Hebrard, Brahim Hnich, Toby Walsh

Paper 74: A Hyper-Arc Consistency Algorithm for the Soft Alldifferent Constraint
Willem Jan van Hoeve

Paper 75: Impact-Based Strategies for Constraint Programming
Philippe Refalo

Paper 77: Propagation Guided Large Neighborhood Search
Laurent Perron

Paper 78: Constraint Propagation as a Proof System
Albert Atserias, Phokion G. Kolaitis, and Moshe Y. Vardi

Paper 81: Generating Robust Schedules through Chaining
N. Policella, A. Oddi, S.F. Smith, and A. Cesta

Paper 84: A Constraint for Bin Packing
Paul Shaw

Paper 93: Completable Partial Solutions in Constraint Programming and Constraint-based Scheduling
Andras Kovacs and Jszsef Vancza

Paper 95: Symbolic Decision Procedures for QBF
Guoqiang Pan, Moshe Y. Vardi

Paper 99: Improved bound computation in presence of several clique constraints
Jean-Francois Puget

Paper 105: (Smart) Look-Ahead Arc Consistency and the Pursuit of CSP Tractability
Hubie Chen and Victor Dalmau

Paper 106: Quantified Constraint Satisfaction and 2-Semilattice Polymorphisms
Hubie Chen

Paper 109: Bounding the Resource Availability of Partially Ordered Events with Constant Resource Impact
Jeremy Frank

Paper 111: Strategies for Global Optimization of Temporal Preferences
Paul Morris, Robert Morris, Lina Khatib, Sailesh Ramakrishnan, Andrew Bachmann

Paper 112: Improved Algorithms for the Global Cardinality Constraint
Claude-Guy Quimper, Alejandro Lopez-Ortiz, Peter van Beek, Alexander Golynski

Paper 117: An Efficient Complete (Weighted) Max-SAT Solver
Zhao Xing and Weixiong Zhang

Paper 120: A Complete Characterization of Complexity for Boolean Constraint Optimization Problems
David Cohen, Martin Cooper, Peter Jeavons

Paper 121: Subproblem Substitutability by Satisfiability Encoding
Steven Prestwich

Paper 122: Controllability of Soft Temporal Constraint Problems
Francesca Rossi and Kristen Brent Venable and Neil Yorke-Smith

Paper 125: Financial Portfolio Optimisation
Pierre Flener, Justin Pearson, and Luis G. Reyna

Paper 130: A Regular Language Membership Constraint for Finite Sequences of Variables
Gilles Pesant

Paper 131: A Domain Consistency Algorithm for the Stretch Constraint
L. Hellsten, G. Pesant, P. van Beek

Paper 132: Speeding Up Constraint Propagation
Christian Schulte and Peter J. Stuckey

Paper 133: Backtrack-Free Search for Real-Time Constraint Satisfaction
J. Christopher Beck, Tom Carchrae, Eugene C. Freuder, and Georg Ringwelski

Paper 138: Monotone Literals and Learning in QBF reasoning
Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella

Paper 141: The Cardinality Matrix Constraint
Jean-Charles Regin and Carla Gomes

Paper 161: ID Walk: A Candidate List Strategy with a Simple Diversification Device
Bertrand Neveu, Gilles Trombettoni, Fred Glover

Paper 169: Solving Non-clausal Formulas with DPLL search
Christian Thiffault, Fahiem Bacchus, Toby Walsh

Paper 178: New Look-Ahead Schemes for Constraint Satisfaction
Kalev Kask, Rina Dechter, and Vibhav Gogate

Paper 184: Global Constraints for Integer and Set Value Precedence
Y.C. Law and J.H.M. Lee

Paper 187: Streamlining Constraint Reasoning
Carla Gomes and Meinolf Sellmann

Paper 192: Quality of LP-based Approximations for Highly Combinatorial Problems
Lucian Leahu and Carla Gomes

Paper 197: Hybrid Set Domains to Strengthen Constraint Propagation and Reduce Symmetries
Andrew Sadler Carmen Gervet

Paper 203: Understanding Random SAT: Beyond the Clauses-to-Variables Ratio
Eugene Nudelman, Alex Devkar, Yoav Shoham, Kevin Leyton-Brown

Short Papers:

Paper 14: Solving the Crane Scheduling Problem using Intelligent Search Schemes
Andrew Lim, Brian Rodrigues, Zhou Xu

Paper 23: Concurrent Dynamic Backtracking for Distributed CSPs
Roie Zivan and Amnon Meisels

Paper 33: A General Extension of Constraint Propagation for Constraint Optimization
Xiaofei Huang

Paper 37: Algorithms for Quantified Constraint Satisfaction Problems
Nikos Mamoulis, Kostas Stergiou

Paper 38: A New Algorithm for Maintaining Arc Consistency after Constraint Retraction
Pavel Surynek, Roman Bartak

Paper 41: Computing the Frequency of Partial Orders
M.R.C. van Dongen

Paper 50: The Tractability of Global Constraints
Christian Bessiere, Emmanuel Hebrard, Brahim Hnich, Toby Walsh

Paper 51: Support inference for generic filtering
Frederic Boussemart, Fred Hemery, Christophe Lecoutre, and Lakhdar

Paper 82: How much backtracking does it take to color random graph? Rigorous results on heavy tails
Haixia Jia and Cristopher Moore

Paper 114: On Tightness of Constraints
Yuanlin Zhang

Paper 127: Variable ordering heuristics show promise
J. Christopher Beck Patrick Prosser Richard J. Wallace

Paper 136: Strong Cost-based Filtering for Lagrange Decomposition Applied to Network Design
Wilhelm Cronholm and Farid Ajili

Paper 140: Improving the applicability of adaptive consistency: Preliminary results 
Marti Sanchez Pedro Meseguer Javier Larrosa

Paper 170 : On-Demand Bound Computation for Best-First Constraint Optimization
Martin Sachenbacher and Brian Williams

Paper 181: Preprocessing Techniques for Distributed Constraint Optimization
Syed Muhammad Ali, Sven Koenig, Milind Tambe

Paper 183: The Impact of AND/OR Search Spaces on Constraint Satisfaction and Counting
Rina Dechter and Robert Mateescu

ABOUT THIS CONFERENCE SERIES

1. Karlsruhe (Germany),
2. Cambridge (United Kingdom),
3. Steyr (Austria),
4. Plattsburgh(USA),
5. Madrid (Spain), and
6. Marseille (France)

SCOPE

Artificial Intelligence and Symbolic Computation are two views and approaches for automating problem solving, in particular mathematical problem solving. The two approaches are based on heuristics and on mathematical algorithmics, respectively. Artificial Intelligence can be applied to Symbolic Computation and Symbolic Computation can be applied to Artificial Intelligence. Hence, a wealth of challenges, ideas, theoretical insights and results, methods and algorithms arise in the interaction of the two fields and research communities. Advanced tools of software technology and system design are needed and a broad spectrum of applications is possible by the combined problem solving power of the two fields.

Hence, the conference is in the center of interest and interaction for various research communities:

• artificial intelligence,
• symbolic computation,
• computer algebra,
• automated theorem proving,
• automated reasoning,
• formal mathematics,
• mathematical knowledge management,
• algorithmic invention and learning,
• logic,
• software technology,
• language and system design,
• implementation and performance issues,
• semantic web technology,
• computer-based math teaching and didactics,
• computer-supported publishing,
• language and system design,
• implementation and performance issues,
• any topics related to the above.

INVITED SPEAKERS

• Alan Bundy (University of Edinburgh, UK)
• Markus Rosenkranz (Johannes Kepler University, Linz, Austria)
• Helmut Schwichtenberg (Ludwig-Maximilian University, Munich, Germany)
• Zbigniew Stachniak (York University, Toronto, Canada)

ACCEPTED PAPERS

• A Paraconsistent Higher Order Logic
      Joergen Villadsen
• Abstraction within Partial Deduction for Linear Logic
      Peep Kungas
• A Decision Procedure for Equality Logic with Uninterpreted Functions
      Olga Tveretina
• Generic Hermitian Quantifier Elimination
      Andreas Dolzmann, Lorenz A. Gilch
• Extending Finite Model Searching with Congruence Closure Computation
      Jian Zhang, Hantao Zhang
• On the Combination of Congruence Closure and Completion
      Christelle Scharff, Leo Bachmair
• Combination of Nonlinear Terms in Interval Constraint Satisfaction Techniques
      Laurent Granvilliers, Mina Ouabiba
• Proving and Constraint Solving in Computational Origami
      Tetsuo Ida, Dorin Tepeneu, Bruno Buchberger, Judit Robu
• Two Revision Methods Based on Constraints: Application to the Flooding Problem
      Mahat Khelfallah, Belaid Benhamou
• An Evolutionary Local Search Method for Incremental Satisfiability
      M.B. Menai
• Solving Equations Involving Sequence Variables and Sequence Functions
      Temur Kutsia
• Verified Computer Algebra in ACL2 (Grobner Bases Computation)
      I. Medina-Bulo, F. Palomo-Lozano, J.A. Alonso-Jimenez, J.L. Ruiz-Reina
• Abstraction-Driven Verification of Array Programs
      D. Deharbe, A. Imine, S. Ranise
• Polynomial Interpretations with Negative Coefficients
      Nao Hirokawa, Aart Middeldorp
• From a Computer Algebra Library to a System with an Equational Prover
      Serge Mechveliani
• New developments in Symmetry Breaking in Search Using Computational Group Theory
      Tom Kelsey, Steve Linton, Colva Roney-Dougal
• Recognition of Whitehead-minimal Elements in Free Groups of Large Ranks
      Alexei D. Miasnikov
• Four Approaches to Automated Reasoning with Differential Algebraic Structures
      Jesus Aransay, Clemens Ballarin, Julio Rubio
• Algorithm-Supported Mathematical Theory Explanation: A Personal View and Strategy
      Bruno Buchberger
• Singularities in Qualitative Reasoning
      Bjorn Gottfried
• An Expert System on Detection, Evaluation and Treatment of Hypertension
      E. Roanes-Lozano, E. Lopez-Vidriero Jr., L.M. Laita, E. Lopez-Vidriero, V. Maojo, E. Roanes-Macias

Concur 2004, the 15th International Conference on Concurrency Theory, takes place at the Royal Society, London, from Tuesday 31 August - Friday 3 September 2004.

The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency, and promote its applications. Interest in this topic is continuously growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations.

Accepted Papers:

Authors are invited to submit papers presenting original and unpublished research work in all areas related to Deduction and Reasoning. The topics of interest of the workshop include, but are not limited to:

- Logic programming and nonmonotonic reasoning 
- Answer Set Programming
- Knowledge and Belief Representation
- Representation of Beliefs
- Satisfiability Problems
- Deduction Techniques
- Automated reasoning 
- Non-classical logics 
- Reasoning about situations and actions 
- Mathematical Structures (Algebraic, Topologic, etc.)
- Natural Language Processing.
- Knowledge Discovery and Data Mining.
- AI in Education and Intelligent Tutoring Systems

SUBMISSION INSTRUCTIONS 

Papers should be written in English, formatted according to the Springer LNCS style and should not exceed 8 pages including references and figures. Submissions in Spanish can also be considered, but we strongly encourage authors to write in English. Please visit the web page for submission details. 

IMPORTANT DATES

Paper submission: 		  August 20th, 2004
Notification of acceptance: 	September 17th, 2004
Final version due: 		    October 1st, 2004
DTS 04: 				 November 22-23rd, 2004 

INTERNATIONAL COMMITTEE

Leopoldo Bertossi, Carleton University, Canada
Antonio Brogi, Universita' di Pisa, Italy
Pedro Cabalar, Universidad de Coruña, Spain
Marina De Vos, University of Bath, United Kingdom
Alfredo Gabaldón, University of Toronto, Canada
Vladik Kreinovich, University of Texas at El Paso, United States 
Alessandro Provetti, Universita' di Milano, Italy
Franco Salvetti, University of Colorado-Boulder, United States

LOCAL COMMITTEE

Jose Arrazola Ramirez, Benemerita Universidad Autonoma de Puebla, Mexico
Cesar Bautista, Benemerita Universidad Autonoma de Puebla, Mexico
Rogelio Davila Perez, Instituto Tecnologico y de Estudios Superiores de Monterrey - Campus Guadalajara, Mexico
Guillermo De Ita, Instituto Nacional de Astrofisica, Optica y Electronica,
Guillermo Morales, Centro de Investigacion y de Estudios Avanzados del IPN, Mexico
Mauricio Osorio, Universidad de las Americas, Puebla, Mexico

WORKSHOP CHAIRS

Dr. Mauricio Osorio Galindo 
Department of Computer Science and Engineering
Universidad de las Americas, Puebla. México
URL: http://www.udlap.mx/~josorio/ 
E-mail: josorio@mail.udlap.mx
 
Dr.  Jose Ramon Enrique Arrazola Ramírez 
Facultad de Ciencias Fisico-Matematicas
Benemerita Universidad Autonoma de Puebla, Mexico
E-mail: arrazola@fcfm.buap.mx

ORGANIZATION AND CONTACT

Claudia Zepeda Cortes, Universidad de las Americas - Puebla  
sc098382@mail.udlap.mx
Magdalena Ortiz, Universidad de las Americas - Puebla
is103378@mail.udlap.mx

OVERVIEW

The view of computational components as `agents' is widely used in contemporary software applications, such as Internet navigation, information management, autonomous process control, and e-commerce. The popularity of the agent paradigm stems not only from its intuitive and appealing nature, capturing the notions of flexibility and evolving behaviour, but also from the range of theories, tools and techniques that have been developed over recent years for agent-based systems.  

However, the increasing use of agents in (business, mission, safety) critical applications, together with the development of infrastructures such as the world-wide web and wireless computing is leading to new problems. Central amongst these is that of the *trustworthiness* of agent software. Can agents be trusted to autonomously make decisions in critical areas? In addition, once large numbers of agents are present, can they work together safely?

Thus, it is important to be able to guarantee predictable behaviour for agent-based systems if these are to be used in critical applications. Verification of agent-based behaviour is a complex problem: the behaviour of individual agents must be verified; collections of agents must be shown to be able to work together effectively; and agents that communicate over wider distances and multiple sites must be shown to retain security properties. Tackling
these problems often requires a large number of diverse techniques, and many such techniques are based on formal logics, thus providing the clear semantic basis for the verification tasks.

The aim of this special issue is to bring together high-quality papers exhibiting leading edge research where a "logic-based" approach is taken to the verification of agent-based systems. We here take a broad view of logic, and consider a wide range of logical verification techniques (incorporating theorem-proving, model checking, algebraic, abstract machines, etc.).


THE JOURNAL

The Journal of Applied Logic (Elsevier) publishes papers in areas of logic which can be applied in other disciplines as well as application papers in those disciplines, the unifying theme being logics arising from modelling the human agent.  


IMPORTANT DATES

Submission deadline:  15th October 2004
Author notification:      15th February 2005
Revised papers due:   15th April 2005


TOPICS OF INTEREST

The topics of interest of this special issue include (but are not limited to)

• verification, modelling and analysis techniques for agent-based or multi-agent systems based on: theorem-proving (including, classical, modal, temporal, higher-order, etc); constraint-based systems; model-checking; abstract machine modelling; algebraic techniques; multi-paradigm approaches; abstraction techniques; links to testing.
• applications of logic-based agent verification, for example in: robotics; autonomous process control; agent-based knowledge/information management; WWW search/navigation/discovery; e-commerce and B2B applications; critical embedded components; telecommunications; security; cooperation, team work and negotiation; analysing evolving/adaptive systems
  

SUBMISSION OF MANUSCRIPTS
 
We invite submission of full (typically, 20-40 pages) high-quality research papers for this special issue. These should neither have been previously published in their full form, nor be under review elsewhere. Submissions consisting of the paper (preferably PDF or Postscript via email but, alternatively, five hard-copies) including an abstract in which the role of logic in the particular approach used is clarified, should be sent to Michael Fisher (address given below) to arrive no later than 15th October 2004. Formatting instructions can be found at the journal's web site.

Queries concerning this special issue should be directed to any of the guest editors. Up-to-date information will also be available from
http://www.csc.liv.ac.uk/~michael/LBAV04


SPECIAL ISSUE EDITORS
    ---------------------

MICHAEL FISHER
Department of Computer Science, 
University of Liverpool, Liverpool L69 7ZF, UK
email: M.Fisher@csc.liv.ac.uk    url:  http://www.csc.liv.ac.uk/~michael

MUNINDAR SINGH
Department of Computer Science, 
North Carolina State University, Raleigh, USA
email: mpsingh@csc.ncsu.edu      url:  http://www.csc.ncsu.edu/faculty/mpsingh

DIANA SPEARS
Department of Computer Science, 
University of Wyoming, Laramie, USA
email:  dspears@cs.uwyo.edu     url:   http://www.cs.uwyo.edu/~dspears

MIKE WOOLDRIDGE
Department of Computer Science, 
University of Liverpool, Liverpool L69 7ZF, UK
email:  M.J.Wooldridge@csc.liv.ac.uk  url: http://www.csc.liv.ac.uk/~mjw

This event will focus on:

1. Techniques that can be used for a general theory of logics (Labelled deductive systems, Kripke structures, Logical matrices, etc.) ;
2. Studies  of classes of logics (Substructural logics, Non monotonic logics, Paraconsistent logics, etc.)
3. Scope of validity and domain of application of fundamental theorems of logic (Completeness, Deduction, Cut-elimination, etc.)
4. Philosophical considerations about the nature of logic and the universality of some logical laws or axioms

The school is intended for advanced students and young researchers. There will be about 20 tutorials on many subjects: combination of logics, multiple conclusion logic, combinatory logic, logics and games,  abstract model theory, logic as language vs. logic as calculus,  category theory for logics, etc.

Invited speakers of the congress will include A.Avron, D.Batens, J.Corcoran, M.Dunn, D.Gabbay, R.Jansana, A.Koslow, V.de Paiva, K.Segerberg.

Contributed papers for the congress can be submitted before October 30, 2004.

More information on the website:  http://www.uni-log.org

You are invited to propose sessions and other contributions to the 16th International Conference on Applications of Declarative Programming and Knowledge Management, INAP2005, Oct 1-3 2005, Waseda University, Japan.

 

Masanobu Umeda, Kyushu Institute of Technology, Japan

Armin Wolf,	Fraunhofer FIRST, Germany

Osamu Yoshie, Waseda University, Japan

Oskar Bartenstein, IF Computer Japan, Japan

Ulrich Geske, Fraunhofer FRIST, Germany

Dietmar Seipel, Universitaet Wuerzburg, Germany

Osamu Takata, Kyushu Institute of Technology, Japa

Suggestions may include any topic of scientific and practical interest. Focus is as with the previous events in Berlin 2004 and Tokyo 2001 on the use of logic programming methods for industrial, commercial, societal applications.

For information on past conferences see http://inap.dialogengines.com
 
Please address suggestions to Oskar Bartenstein oskar@ifcomputer.co.jp or any other member of the INAP community.

Oskar Bartenstein  oskar@ifcomputer.co.jp http://www.ifcomputer.co.jp

• Innovative applications of declarative languages.
• Declarative domain-specific languages and applications.
• Practical applications of theoretical results.
• New language developments and their impact on applications.
• Evaluation of implementation techniques on practical applications.
• Novel implementation techniques relevant to applications.
• Novel uses of declarative languages in the classroom.
• Practical experiences.

The 16th Int. Conf. on Rewriting Techniques and Applications (RTA'05)  will collocate with the 7th International Conference on Typed Lambda Calculi and Applications (TLCA'05) as part of the Federated Conference on Rewriting, Deduction and Programming (RDP'05).


IMPORTANT DATES:

Deadline for electronic submission of title and abstract:

Nov    12, 2004

Deadline for electronic submission of papers:

Nov    19, 2004

Notification of acceptance of papers:

Jan    14, 2005

Deadline for final versions of accepted papers:

 Feb     4, 2005

Conference:

Apr 19-21, 2005

RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include (but are not limited to):

• APPLICATIONS:
• case studies; rule-based (functional and logic) programming; 
• symbolic and algebraic computation; theorem proving;
• system synthesis and verification; proof checking.
• FOUNDATIONS:
• matching and unification; narrowing; completion techniques;
• strategies; constraint solving; explicit substitutions; tree automata.
• FRAMEWORKS:
• string, term, and graph rewriting; lambda-calculus and
• higher-order rewriting; proof nets; constrained
• rewriting/deduction; categorical and infinitary rewriting.
• IMPLEMENTATION:
• compilation techniques; parallel execution; rewriting tools.
• SEMANTICS:
• equational logic; rewriting logic.
  

INVITED TALKS 
Invited talks will be given at RTA'05 by:

• Amy Felty (Ottawa)
• Yoshihito Toyama (Sendai)
• Philip Wadler (Edinburgh)

BEST PAPER AWARDS:
An award of 100,000 Yen will be given to the best paper or papers as decided by the PC. 


RTA'04 PROGRAM COMMITEE:

• Franz Baader (Dresden)
• Mariangiola Dezani (Torino)
• Juergen Giesl (Aachen, Chair)
• Bernhard Gramlich (Vienna)
• Florent Jacquemard (Cachan)
• Claude Kirchner (Nancy)
• Pierre Lescanne (Lyon)
• Aart Middeldorp (Innsbruck)
• Hitoshi Ohsaki (Amagasaki)
• Vincent van Oostrom (Utrecht)
• Christine Paulin-Mohring (Orsay)
• Frank Pfenning (Pittsburgh)
• Femke van Raamsdonk (Amsterdam)
• Mark-Oliver Stehr (Urbana)
• Rakesh Verma (Houston)
• Andrei Voronkov (Manchester)

RTA'05 SUBMISSIONS:
Submissions must be original and not submitted for publication elsewhere. Submission categories include regular research papers and system descriptions. Also problem sets and submissions describing interesting applications of rewriting techniques will be very welcome. The page limit is 15 pages (10 pages for system descriptions).
As usual, accepted papers will appear in the Springer-Verlag Lecture Notes in Computer Science series. More information about paper submission is available at the RTA'05 web page.

LOCATION, TRAVEL, ACCOMODATION, AND REGISTRATION
The conference takes place in Nara park, which is one of the most important cultural sights of Japan with some of the oldest and most impressive temples  and shrines. Airfares from Europe or the US to Japan are not expensive in  mid-April and the conference will offer reasonably priced accommodation and low registration fees. 


RTA'05 PROGRAM CHAIR:
Juergen Giesl
LuFG Informatik II 
RWTH Aachen
Ahornstr. 55
52074 Aachen 
Germany
giesl@informatik.rwth-aachen.de


RTA'05 CONFERENCE CHAIR:
Hitoshi Ohsaki
AIS
Japan
ohsaki@ni.aist.go.jp

VMCAI provides a forum for researchers from the communities of Verification, Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine the three areas. With the growing need for formal methods to reason about complex, infinite-state, and embedded systems, such hybrid methods are bound to be of great importance.

The program of VMCAI'05 will consist of invited tutorials, refereed papers, invited lectures on -Perspectives in Program Verification- and invited demonstrations of -Tools for Program Verification-.

Papers are solicited reporting new results as well as experimental evaluation and comparisons of existing techniques. Topics include but are not limited to:

• program verification
• program certification
• model checking
• debugging techniques
• abstract interpretation
• abstract domains
• static analysis
• type systems
• deductive methods
• optimization
  

Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming.

Papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings.

Submission instructions:
All submissions must be performed electronically at http://www.polytechnique.fr/vmcai05/ (use of this page requires a recent, script-enabled HTML browser). Submitted papers should be at most (LNCS style) 15 pages excluding bibliography and well-marked appendices. Program committee members are not required to read the appendices, and thus papers should be intelligible without them.

Publication:
The proceedings will be published by Springer in the Lecture Notes in Computer Science series (see the LNCS Author's Instructions
 http://www.springer.de/comp/lncs/authors.html ).  Thus, adhering to that style already in the submission is strongly encouraged.  Papers should be
submitted either in PostScript or PDF format and they should be interpretable by Ghostscript or Acrobat Reader.  Papers must be printable on either A4 paper or US letter, and preferably on both.

Journal Special Issue:
Selected papers will be invited to a Journal Special Issue.

Best Paper Award:
Starting this VMCAI'05, the program committee may select papers accepted to the conference as VMCAI Best Papers.

Important dates:

Deadline for submissions :

September 6, 2004, 19:00 UTC/GMT

Notification of acceptance or rejection: 

October 11, 2004

Deadline for reception of the final versions :

November 8, 2004

The conference : 

January 17-20, 200

Program Committee:

Agostino Cortesi 	Università Ca'Foscari di Venezia (I)
Radhia Cousot  	 	CNRS / École Polytechnique (F)
E. Allen Emerson        University of Texas, Austin (USA)
Roberto Giacobazzi      Università degli Studi di Verona (I)
Chris Hankin 	   	Imperial College (UK)
Warren A. Hunt 	   	University of Texas, Austin (USA)
Ken McMillan 	   	Cadence Berkeley (USA)
David Monniaux 	   	CNRS / École Normale Supérieure (F)
Amir Pnueli 	   	Weizmann Institute of Science (IL)
Andreas Podelski        Max-Planck-Institut für Informatik (G)
Francesco Ranzato 	Università di Padova (I)
Hanne Riis Nielson    	Technical University of Denmark (DK)
Shmuel Sagiv 	   	Tel-Aviv University (IL)
Bernhard Steffen        Universität  Dortmund (G)
Reinhard Wilhelm    	Universität des Saarlandes (G)


Program Chair:

Email: 	Radhia.Cousot@polytechnique.fr
Post: 	Radhia Cousot
        École Polytechnique - STIX, 91128 Palaiseau cedex, France
Fax: 	+ 33 (0)1 69 33 30 50
Phone: 	+ 33 (0)1 69 33 45 95


VMCAI Steering Committee:

Agostino Cortesi 	   	Università Ca'Foscari di Venezia (I)
E. Allen Emerson                University of Texas, Austin (USA)
Giorgio Levi                    Università di Pisa (I)
Thomas W. Reps                  University of Wisconsin-Madison (USA)
Andreas Podelski                Max-Planck-Institut für Informatik (G)
David A. Schmidt                Kansas State University (USA)
Lenore Zuck                     New York University (USA)

Overview

Constraints have emerged as the basis of a representational and computational paradigm that draws from many disciplines and can be brought to bear on many problem domains.

Scope

The track is concerned with all aspects of computing with constraints including algorithms, applications, environments, languages, models, and systems. Contributions are welcome from any discipline concerned with constraints, including artificial intelligence, combinatorial algorithms, computational logic, concurrent computation, databases, discrete mathematics, operations research, programming languages, and symbolic computation. We also solicit papers from any domain employing constraints, including computational linguistics, configuration, decision support, design, diagnosis, graphics, hardware verification, molecular biology, planning, qualitative reasoning, real-time systems, resource allocation, robotics, scheduling, software engineering, temporal reasoning, vision, visualization, and user interfaces. Papers that bridge disciplines or combine theory and practice or discuss novel reasoning methods are especially welcome. A special attention is focused around the use of constraint technologies in the networking, wireless and internet fields.

Submissions

We would like to invite authors to submit papers on research on constraint solving and programming, with particular emphasis on assessing the current state of the art and identifying future directions.

Preliminary guidelines

At least three reviewers will be assigned to each submission to the track. Accepted papers are published by ACM in both printed form and CD-ROM; they are also available on the Web through the ACM Digital Library. Once accepted, papers must fit within five (5) two column pages (please check the author kit on the main SAC website: the format is usually the format used in the ACM templates), with the option (at additional expense) to add three (3) more pages.
A second set of selected papers, which did not get accepted as full papers, will be accepted as posters and will be published as extended 2-page abstracts in the symposium proceedings.

Authors of accepted papers must be prepared to sign a copyright statement and must pay the registration fee and guarantee that their paper will be presented at the conference.

Paper submissions should be sent (as an attached PDF file) to:

We strongly suggest to use for submission the available camera ready templates, and adhere to the 5 page limitation.

Registration is required for paper and poster inclusion in the Conference Proceedings, and for event attendance. (please see Registration Page)

Important Dates

The proposed schedule of important dates for the track is as follows:

Organising Committee

Stefano Bistarelli (Primary Contact)
Dipartimento di Scienze
Università degli studi "G. D'Annunzio" di Chieti-Pescara, Italy
Email: bista@sci.unich.it
Web: http://www.sci.unich.it/~bista/
and
Istituto di Informatica e Telematica
C.N.R. Pisa, Italy
Email: stefano.bistarelli@iit.cnr.it

Eric Monfroy
LINA
University of Nantes,France
Email: Eric.Monfroy@lina.univ-nantes.fr
Web: http://www.sciences.univ-nantes.fr/info/perso/permanents/monfroy/

Software demos due on 21 March, 2005