by Polina Kutznetsova,
SUNY Stony Brook,
USA
Introduction
The Third International ALP/GULP Spring School on Computational Logic, ISCL 2011, has been held at University Residential Centre of Bertinoro during April 10-15.
The School targeted doctoral students, exceptional Master students, and other interested researchers. It provided a comprehensive introduction to different research topics including interesting discussions and brainstorming activities. Several student sessions, dedicated to writing paper abstracts or projects proposals, were also held. Besides lectures and student sessions there were organized few social trips and events. Social events included joint meals and a trip to Urbino.
The School has invited internationally renowned researchers to speak on topics from their field of expertise.
All lectures were distributed evenly over the week.
Constraint Languages for Parametrized Verification: Bags, Words, Trees, and Graphs, by Giorgio Delzanno
Professor Giorgio Delzanno started his lectured by introducing the Model Checking, which is used for software ans hardware verification. The main idea is to check is a certain property holds for a system, for example safety requirement.
Professor Delzanno gave an example of multitasking computation where checking for absence race conditions. He stated that a system can be modeled as a collection of states with transition relations between them. The goal is to test system for a certain property called specification.
Lectures included such topics as verification of Finite-state Systems and Infinite-state Systems. For Finite-state Systems Computation Tree Logic and Model Checking Algorithms can be used. For verification of Infinite-state Systems methods are Constraint-based Model Checking and Parameterized Verification. Latter includes Unorders Systems, Linear Systems, Trees and Graphs Topologies.
Professor Delzanno in his lectures covered such topics as Computation Tree logic and Model Cheking, Constraint-based Model Checking, Verification of Parameterized Systems and Approximated Verification Parameterized Systems.
Description Logics, by Enrico Franconi
Professor Enrico Franconi in his lectures introduced the basic notion of Ontology as a conceptual schema that specifies a set of constraints. For describing ontologies he chose to use UML class diagrams that can be considered as ontology languages. Using UML he describes relational database schema. Professor Franconi stated that constraints can be seen as first-order logic formulas. If database is incomplete then it can be expressed by means of logic formulas. To answer queries in case of incomplete information we need entailment.
Professor Franconi talked about reasoning with conceptual schema, when additional constraints can be inferrend from a schema. He continued with encoding conceptual schemas in logic.
The next step is querying database with constraints, i.e. answering a query over the conceptual schema vocabulary.
Professor Franconi talked about Databases with conceptual schema with exact views or DBox. Another type of schema is ABox, or database with sound views, i.e. incomplete information about some term appearing in the conceptual schema.
Professor Enrico Franconi showed that answering queries with ABox systems can lead to answers that do not scale to standard database answers. Moreover with ABox queries are not compositional with certain answer semantic. For example, a programmer can try to get all information from some tables of database and then perform an operation like projection on them. This can give an answer that is different from the one obtained when performing projection on database side. Another example that shows disadvantages of ABox is map-coloring problem, when querying with ABox always gives an answer, because potentially we can have infinite amount of colors. But this is not a solution to graph-coloring problem.
The problem with DBoxes is that query answering with it is co-NP-hard and is much harder than with ABoxes.
At the end of his lectures Professor Franconi showed that DBox can be computationally efficient.
Computational Logic and Human Thinking: How to be Artificially Intelligent, by Robert Kowalski
Professor Robert Kowalski introduced Abductive Logic Programming (ALP) agent model, which includes agent cycle, model-theoretic and operational semantics, deciding between alternatives. He looked at ALP agent as a variant of BDI agents. Agents use their beliefs to attain their desires (goals) by generating intentions, which are selected plan of actions. In ALP agents’ beliefs and desires are both represented as conditionals in the clausal form of logic. Professor introduced operational semantics for ALP agents. An agent observes then performs forward reasoning to derive conclusions from observations and derive achievement goal. Then it performs backward reasoning reducing the goals to the consecutive sub-goals. If the last action is an atomic action and the action is executed successfully, then the action makes the achievement goal and this instance if the maintenance goal both true. ALP agents also use abduction, which is the task of generating assumptions to explain observations. Backward reasoning from the observation generates an assumption.
Talking about Psychology Professor Kowalski argued that Human Thinking can be modeled using logic. His stated that there is a gap between natural language and language of thoughts and this gap cause doubts about humans being logical. He mentioned Wason selection task, suppression task and representation of cause and effect.
Then Professor Kowalski gave a talk about Language of Thought (LOT). He stated that the relation between natural language and LOT corresponds to relationship between first-order logic and ALP and considers ALP as the Language of Thought. He talked about ALP clausal logic as a connectionist model of the mind.
In the next lectures Professor Kowalski talked about Semantics of the clausal logic of ALP and Logic of Abductive Programming.
After that Professor Kowalski returned back to Psychology explaining that the meaning of natural language conditional depends on whether they are interpreted as beliefs or as goals.
At the end of his lectures Professor Kowalski compared ALP and BDI agents. They share the same agent cycle but differ in knowledge representation. BDI agents, for example, use destructively updated database, while in ALP agents the database is non-destructive and observations are needed to access the current state of the world.
Unity in Computational Logic, by Dale Miller
Professor Dale Miller in his lectures talked about different fragments of computational logic, his goal was to organize all of them into a large framework and view different approaches as certain choices withing this framework.
He started his lecture with an introduction to the roles of logic in computation and division of computational logic into several different fragments. He highlighted the difference between functional programming and logic programming. For functional programming programs are proofs and computation is proof normalization. While for logic programming programs are theories and computation is the search for proofs. He stated that large percentage of computational systems based on logic is implemented using one of the 2 logics: Classical and Intuitionistic Logic.
Professor Miller mentioned that there is also a division between computation, model checking and theorem proving. Being part of a common framework allows, for example, mixing model checking and theorem proving or mixing computation and deduction.
In his following lectures Professor Miller gave some introduction on sequent calculus. Then he concentrated on proof theory for logic programming. He talked about a single proof system for classical and intuitionistic logic, which can give classical and intuitionistic proofs. In the next lectures Professor introduces focused proof systems for intuitionistic logic and focused proof systems for classical logic.
In the last lecture Professor Miller talked about equality and fixed points in proof systems.
Constraint Programming and Optimization Systems, by Pascal Van Hentenryck
Professor Pascal Van Hentenryck in his lectures focused on Constraint Programming and its improvement techniques. He introduced many examples of algorithms, such as
- map-coloring
- 8 queens problem
- knight tour
- jobs scheduling
- games matches scheduling
- scheduling of actors and scenes
- sudoku puzzle
and many others
Each of these algorithms is based on exploring many states of search tree, which is formed by assigning to chosen variables values from their domains. The main idea was to reduce search space. For example, reducing the domain of variables, adding redundant constraints.
One of the aspects of reducing search space is choosing the order of considered variables. We can chose a variable that has the smallest domain, also we can chose value for the variable that reduces domain of other variable the least. But in some cases it is hard to find the best ordering. For these cases randomized ordering can be used.
Another improvement to some algorithms is to use redundant constraints, which help to prune search tree on earlier stages.
In his lectures Professor Van Hentenryck highlighted that number of problems that NP-complete can gain a significant improvement in performance when using Constraint Programming with several techniques to prune search tree.
Student session
Besides lectures there were organized a series of student sessions. Students had a choice among two workshops: Writer’s Workshop and Project Workshop.
Writes’s Workshop goal was to teach students how to write an abstract for a paper. Students submitted samples of abstracts and discussed them in groups, making suggestions on how to improve an abstract and make it clear and easy to understand for a reader.
Project Workshop focus is on teaching students how to write a project proposal. It was mostly targeted to senior PhD students, post-docs and research assistants.
Trips and events
School organizers scheduled a trip to the city of Urbino. We visited the palace of Federico da Montefeltro, who was the lord of the city during Renaissance. A guide led us on a tour through the palace, where we saw beautiful paintings and arts, including portraits of Federico himself and one of Raphael’s paintings.
After palace we visited city’s panorama, where we could see an amazing view of the city.
Conclusions
ISCL school organized in conjunction with DALT was an amazing experience and a great opportunity for many students all over the world. The set of interesting lectures helped students to get familiar with interesting topics in different research areas. While social trips and events gave students time and opportunity to communicate with each other and lecturers.
Thanks to sponsor support, ISCL 2011 were able to help participation of students at all levels. About 30 students attended ISCL 2011 which was hold in conjunction with DALT 2011, The First International Spring School on Declarative Agent Languages and Technologies, that was attended by about 30 students.