Helena Rasiowa

on her 100th anniversary

of birth

SPECIAL SESSION

In memory

of

Helena Rasiowa

Fifty years ago in 1967, when I started my PhD in Edinburgh, resolution logic, developed by Alan Robinson, was lighting the way for automated theorem-proving. Cordell Green, working on his PhD at Stanford was showing how resolution could also be applied to such AI application areas as question-answering, robot plan-formation and automatic programming. These high hopes for resolution logic were challenged by Carl Hewitt and Terry Winograd at MIT, applying procedural representations of knowledge to planning and natural language understanding. The resulting intellectual skirmishes between advocates of logical and procedural approaches led to the development of logic programming and Prolog in 1972.

My own contributions to these developments came from trying to reconcile my work with Donald Kuehner on SL resolution with the procedural representations developed at MIT. They were greatly assisted by my interactions with Alain Colmerauer in Marseille. During the 1970s, logic programming drew support from a small but enthusiastic community of researchers, mainly in Europe. But in the early 1980s, it became the focus of world-wide attention, when it was chosen as the software for the 10 year Japanese Fifth Generation Computer System (FGCS) Project, which aimed to develop AI applications using massively parallel computer architectures. The FGCS Project did not achieve its objectives, and opinions are still divided about whether FGCS was simply ahead of its time.

I will argue in my talk that, although logic programming was intended from its very origins to reconcile logical and procedural representations of knowledge, the fundamental challenge to Computer Science of understanding that relationship is still unresolved. I will also present some suggestions for dealing with this challenge in the future.

---

Robert Kowalski is Emeritus Professor at Imperial College London. He studied at the University of Chicago, the University of Bridgeport, Stanford University, the University of Warsaw, and the University of Edinburgh, where he completed his PhD in 1970. He joined Imperial College in 1975.

Kowalski’s early research was in the field of automated theorem-proving, leading to the development of logic programming in the early 1970s. His later research has focused on the use of logic programming for knowledge representation and problem solving, including work on the event calculus, legal reasoning, abductive reasoning and argumentation. He is currently working with Fariba Sadri on developing the logic and computer language LPS. The philosophical background for this work is presented in his 2011 book Computational Logic and Human Thinking – How to be Artificially Intelligent. An open-source, online prototype is accessible from http://lps.doc.ic.ac.uk/.

During the 1980s, Kowalski was heavily involved in the British response to the Japanese Fifth Generation Project. He also served as an advisor to the UNDP Knowledge Based Systems Project in India, and to DFKI, the German Institute for Artificial Intelligence. Recently he has been an advisor to the Department of Immunization, Vaccines and Biologicals, of the World Health Organization in Geneva.

Kowalski is a Fellow of the Association for the Advancement of Artificial Intelligence, the European Association for Artificial Intelligence, and the Association for Computing Machinery. He received the IJCAI (International Joint Conference of Artificial Intelligence) award for Research Excellence in 2011, and the Japanese Society for the Promotion of Science Award for Eminent Scientists for 2012-2014.

Justification logic began with Sergei Artemov’s work providing an arithmetic semantics for intuitionistic logic. As part of that work, a small number of explicit modal logics were introduced—logics in which there was a structure of terms that kept track of not just what was a necessary truth, but why it was necessary. These explicit modal logics were connected with standard modal logics such as S4, T, K, and others using Realization Theorems, essentially saying that modal operators concealed an underlying informational structure. Since Artemov’s work, the phenomenon of justification logic has turned out to be very broad. For instance, I have shown that infinitely many modal logics have justification counterparts. In my talk I will sketch the basics and try to give some of the ideas behind formal justification proofs, justification semantics, and Realization theorems.

---

Melvin Fitting was born in Troy, New York, in 1942. His undergraduate degree was from Rensselaer Polytechnic Institute, in mathematics, and his 1968 PhD was supervised by Raymond Smullyan, at Yeshiva University. His dissertation became his first book, Intuitionistic Logic, Model Theory, and Forcing (1969). He has worked in many areas including intensional logic, semantics for logic programming, theory of truth, but much of his work has involved developing tableau systems for non-classical logics, thus generalizing the classical systems of his mentor Smullyan. In 2012 he received the Herbrand Award from the Conference on Automated Deduction, largely for this work. He was on the faculty of the City University of New York from 1969 to his retirement in 2013, at Lehman College, and at the Graduate Center, where he was in the Departments of Mathematics, Computer Science, and Philosophy. He has authored or co-authored 9 books as well as numerous research papers, covering philosophical logic, computability, automated theorem proving and, with Raymond Smullyan, set theory. He is currently an emeritus Professor, and very much active.

We present an operational semantics for time-aware business processes, that is, processes modeling the execution of business activities, whose durations are subject to linear constraints over the integers. We assume that some of the durations are controllable, that is, they can be determined by the organization that enacts the process, while others are uncontrollable, that is, they are determined by the external world.

Then, we consider controllability properties, which guarantee the completion of the enactment of the process, satisfying the given duration constraints, independently of the values of the uncontrollable durations. Controllability properties are encoded by quantified reachability formulas, where the reachability predicate is recursively defined by a set of Constrained Horn Clauses (CHCs). These clauses are automatically derived from the operational semantics of the process.

Finally, we present two algorithms for solving the so called weak and strong controllability problems. Our algorithms reduce these problems to the verification of a set of quantified integer constraints, which are simpler than the original quantified reachability formulas, and can effectively be handled by state-of-the-art CHC solvers.

---

Alberto Pettorossi received the Laurea Degree in Electronic Engineering on 1971 from the University of Roma "Sapienza" (Italy). In 1984 he received the Ph.D. degree in Computer Science from Edinburgh University (Scotland). From 1975 until 1988 he was a research worker of the Italian National Research Council. Since 1988 he has been professor of Theoretical Computer Science at the University of Rome "Tor Vergata".

The research activity of Prof. Pettorossi is mainly concerned with the development of methodologies for the transformation, derivation, verification, and synthesis of correct and efficient programs, both in the area of functional languages and the area of logic and concurrent languages. In past years Prof. Pettorossi was also interested in rewriting systems and algebraic-categorical semantics of concurrent programs.

Currently, together with his collaborators, among whom is Dr. Maurizio Proietti of IASI-CNR (Rome, Italy), he is interested in the development of techniques and tools for proving properties of distributed programs, business processes, and in general infinite state systems, by applying the program transformation methodology.

He is author or coauthor of more than one hundred fifty scientific papers. He has written a few chapters of scientific books and he has been the editor of three books. He wrote books for university courses on: Automata Theory and Formal Languages, Predicate Logic and Logic Programming, Foundations of Computing, Pascal Programming, C++ Programming, Java Programming, Concurrent Programming, Theory of Searching, Parsing, and Matching, and Semantics of Programming Languages.

Prof. Pettorossi is an editor of the Fundamenta Informaticae Journal. He is an emeritus member of the IFIP Working Group 2.1 on programming languages. He took part in various scientific projects with national and international institutes, and among them, Edinburgh University (Scotland), University of Warsaw (Poland), and the IASI-CNR Institute in Rome (Italy). He has been member of various international committees for doctorate degrees, faculty positions, and research grants. He is member of the board of the Italian GULP Association (Users and Researchers on Logic Programing). He took part in many programme committees for national and international congresses and he has been referee of various international journals. He has been invited speaker and programme chairman for some international conferences. In 1988 he has received, together with Professor Andrzej Skowron, a price of the Polish Mathematical Society.

Abstract Calculus of programs (or algorithmic logic) is a formal logical system that serves as foundation in tasks of specifying and veryfying of software. The language of the calculus contains formulas able to express semantic properties of programs (aka specification) such as halting property, correctness, weakest precondition, strongest postcondition, equivalence of programs etc. The axioms and the inference rules allow to construct proofs, hence enabling verification of software against its specification. Algorithmic theories built on the base of algorithmic logic are formal counterparts of notion of classes in object programming. We shall briefly present the results of four ph.d. students of Helena Rasiowa: G. Mirkowska, A. Kreczmar, L.Banachowski and A. Salwicki and prof. Rasiowa on algorithmic logic.

---

Andrzej Salwicki graduated under direction of Karol Borsuk. Since 1959 he is programming computers and doing research on laws of programming. For over 30 years he was asistant professor then professor in Institute of Informatics Warsaw University. He inspired two research programs: algorithmic logic (aka calculus of programs) since 1968 and Loglan, an object and distributed programming language (since 1977). Both projects are still alive. Promoted 17 doctors, 12 of them are professors at universities in Poland, Canada, Germany, Mexico and US. Published 2 books on algorithmic logic (jointly with Grażyna Mirkowska) and several papers. He maintains a repository of AL and Loglan: http://lem12.uksw.edu.pl.

Copyright © 2016 Concurrency Specification and Programming 2017

Design by KingArchee