| ICLP06 | Twenty Second International Conference on Logic Programming Seattle, August 17 - 20, 2006 |
ICLP on Saturday, August 19th
Session 6: Special Interest (09:00‑09:30)
Chair:
Mirek Truszczynski
| 09:00‑09:30 | Péter Szabó
(PhD student, Budapest University of Technology and Economics,Department of Computer Science and Information Theory) Péter Szeredi (associate professor, Budapest University of Technology and Economics,Department of Computer Science and Information Theory) Improving the ISO Prolog standard by analysing compliance test results Part 1 of the ISO Prolog standard (ISO/IEC 13211) published in 1995 covers the core of Prolog including syntax, operational schemantics, streams and some built-in predicates. Libraries, DCGs, and global mutables are current standardisation topics. Most Prolog implementations provide an ISO mode in which they adhere to the standard. Our goal is to improve parts of the Prolog standard already published by finding and fixing ambiguities and missing details. To do so, we have compiled a suite of more than 1000 test cases covering part 1, and run it on several free and commercial Prolog implementations. In this study we summarize the reasons of the test case failures, and discuss which of these indicate possible flaws in the standard. We also discuss test framework and test case development issues specific to Prolog, as well as some portability issues encountered. |
Invited Talk (09:30‑10:30)
Chair:
Mirek Truszczynski
Break (10:30‑11:00)
Session 7: Applications I (11:00‑12:30)
Chair:
Enrico Pontelli
| 11:00‑11:30 | Martin Brain
(University of Bath) Tom Crick (University of Bath) Marina De Vos (University of Bath) John Fitch (University of Bath) TOAST: Applying Answer Set Programming to Superoptimisation Answer set programming (ASP) is a form of declarative programming particularly suited to difficult combinatorial search problems. However, it has yet to be used for more than a handful of large-scale applications, which are needed to demonstrate the strengths of ASP and to motivate the development of tools and methodology. This paper describes such a large-scale application, the TOAST (Total Optimisation using Answer Set Technology) system, which seeks to generate optimal machine code for simple, acyclic functions using a technique known as superoptimisation. ASP is used as a scalable computational engine to handle searching over complex, non-regular search spaces, with the experimental results suggesting that this is a viable approach to the optimisation problem and demonstrates the scalability of a variety of solvers. |
| 11:30‑12:00 | Susanne Grell (Universität Potsdam, Institut für Informatik) Torsten Schaub (University of Potsdam) Joachim Selbig (Universität Potsdam, Institute für Biologie und Informatik) Modelling biological networks by action languages via answer set programming We describe an approach to modelling biological networks by action languages via answer set programming. To this end, we propose an action language for modelling biological networks, building on previous work by Baral et al. We introduce its syntax and semantics along with a translation into answer set programming. Finally, we describe one of its applications, namely, the sulfur starvation response-pathway of the model plant Arabidopsis thaliana and sketch the functionality of our system and its usage. |
| 12:00‑12:30 | Petra Schwaiger
(University of Passau) Burkhard Freitag (University of Passau) Using Answer Set Programming for the Automatic Compilation of Assessment Tests Life-long learning is more and more playing a key role for economical, personal and social success. Therefore the management and development of skills and knowledge is of premier importance in industry and, on the other hand, a major expense factor. So called examination management systems assist teachers and trainers through an automatic compilation of documents, in particular assessment tests, based on user defined requirements and constraints and thus help reduce costs. In this paper we present and discuss a solution of the underlying general problem using Answer Set Programming and show the power and advantages of our approach. |
Lunch break (12:30‑14:00)
Session 8: Semantics (14:00‑16:00)
Chair:
Manuel Hermenegildo
| 14:00‑14:30 | Maarten van Emden
(University of Victoria) Compositional Semantics for the Procedural Interpretation of Logic The composition of logic programs out of clauses has been studied semantically, but not the composition of a single clause out of its components. Structurally, a logic program can be regarded as a sentence in clausal form. In his procedural interpretation of logic programs, Kowalski has shown that a positive Horn clause can be viewed as a procedure in the programming sense. This interpretation suggests a composition operator for logic programs, the one where a clause results from composing a head with a body. In this paper we give more detail to the procedural interpretation by giving an algebraic characterization of Kowalski's composition. In addition, we give algebraic characterizations of the composition of goals in a procedure body and for the composition of the predicate symbol with the argument tuple within a goal. A starting point for the semantic operator corresponding to composition of goals is provided by Tarski's cylindric algebra semantics for first-order predicate logic. Tarski's construction is briefly reviewed and suitably modified. The additional semantic operators are shown to be correct with respect to the fixpoint semantics of the logic program as a whole. |
| 14:30‑15:00 | Luke Simon (University of Texas at Dallas) Ajay Mallya (University of Texas at Dallas) Ajay Bansal (University of Texas at Dallas) Gopal Gupta (University of Texas at Dallas) Coinductive Logic Programming We extend logic programming's semantics with the semantic dual of traditional Herbrand semantics by using greatest fixed-points in place of least fixed-points. A query then involves using coinduction to check inclusion in the greatest fixed-point that constitutes the program's semantics. The resulting coinductive logic programming language is syntactically identical to, yet semantically subsumes logic programming with rational terms and lazy evaluation. We give the declarative and operational semantics of such a coinductive logic programming language and prove them equivalent. Our operational semantics lends itself to an elegant and efficient goal directed proof search in the presence of infinite (but rational) terms and proofs. Coinductive logic programming has applications to rational trees, verifying infintary properties, lazy evaluation, concurrent logic programming, model checking, bisimilarity proofs, Answer Set Programming (ASP), etc. Finally, an outline of a prototype implementation realized by modifying YAP Prolog's engine at the WAM level is also described. |
| 15:00‑15:30 | Pedro Cabalar
(Corunna University) Sergei Odintsov (Sobolev Institute of Mathematics) David Pearce (Universidad Rey Juan Carlos) Agustin Valverde (University of Malaga) Analysing and Extending Well-Founded and Partial Stable Semantics using Partial Equilibrium Logic In [COP06] a general nonmonotonic formalism called "partial equilibrium logic" (PEL) is proposed as an adequate logical foundation for the well-founded semantics (WFS) of logic programs. In particular [COP06] identifies and axiomatises a non-classical logic called HT2 and shows that on normal logic programs a natural class of minimal models in HT2, called "partial equilibrium models", coincide with partial stable (p-stable) models. For the well-founded and p-stable semantics, therefore, PEL and HT2 provide the means to analyse properties such as strong equivalence and other logical features of programs. They also enable one to extend the definition of WFS and the p-stable semantics to arbitrary propositional theories. This paper continues the work of [COP06] by studying properties of PEL applied to normal and disjunctive logic programs and programs with nested expressions; in particular showing that PEL is equivalent to p-stable semantics on disjunctive programs. Also the strong equivalence theorem for PEL is extended here to cover special subclasses of models. In addition, we consider some proof-theoretic and computational issues, including complexity results and a method to reduce PEL to ordinary equilibrium logic. [COP06] P. Cabalar, S. Odintsov & D. Pearce. Logical Foundations of Well-Founded Semantics. In proceedings of KR'2006 (to appear). |
| 15:30‑16:00 | James Cheney (University of Edinburgh) The Semantics of Nominal Logic Programs Nominal logic programming is a form of logic programming with "concrete" names and binding, based on nominal logic, a theory of alpha-equivalence founded on swapping and freshness constraints. Previous papers have employed diverse characterizations of the semantics of nominal logic programs, including operational, denotational, and proof-theoretic characterizations. In this paper we give a uniform presentation of these characterizations and prove appropriate soundness and completeness results. We also give some applications of these results. |
Break (16:00‑16:30)
Keynote Session (16:30‑17:30)
Chair:
Wolfram Schulte, Moshe Vardi
Location:
Grand Ballroom B/C
| 16:30‑17:30 | David Harel
(Weizmann Institute) Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs [ppt] We concentrate on executing scenario-based, inter-object programs. The basic play-out method for live sequence charts (LSCs), which we proposed several years ago and implemented in the Play-Engine tool, deals with the nondeterminism inherent in such programming like racing conditions. It thus cannot correct unsuccessful choices it makes. The talk discusses three more recent and more sophisticated ways to run LSCs, and by extension to execute scenario-based models and programs in general. Interestingly, and somewhat unusually, these three methods use, respectively, ideas from three quite separate fields of computer science: verification (model-checking), artificial intelligence (planning algorithms) and programming methods (Aspect-oriented programming). |
ALP Business Meeting (17:45‑19:00)
