Sergei Artemov
Proof carrying formulas and the Logic of Proofs LP were invented in the 1990s for solving a problem of the intended provability semantics of the modal and intuitionistic logic left open by Goedel. In this talk we will discuss possible applications of the Logic of Proofs in Computer Science. In the area of knowledge representation LP allows us to approach classical logical omniscience problem, which addresses a failure of the traditional logic of knowledge to distinguish between facts which are given, and the ones which can be only obtained after a long derivation process. The proof carrying formulas of LP naturally make this distinction. In the area of lambda-calculi and typed theories, proof carrying formulas bring in a much richer system of types capable of iterating the type assignment. We introduce and discuss the Reflexive Combinatory Logic (RCL) which provides a basic model of a programming language with a built-in compiler.
Arnon Avron
The ordinary concept of a multiple-valued matrix is generalized by introducing non-deterministic matrices (Nmatrices), in which non-deterministic computations of truth-values are allowed. It is shown that some important logics for reasoning under uncertainty can be characterized by finite Nmatrices, although they have only infinite characteristic ordinary (deterministic) matrices. On the other hand, a strong connection is established between the admissibility of the cut rule in canonical Gentzen-type propositional systems, non-triviality of such systems, and the existence of sound and complete non-deterministic two-valued semantics for them.
Mel Fitting
A well-known problem with formal logics of knowledge is "logical omniscience," one knows too much. This breaks down into two subproblems: one knows all tautologies, and one's knowledge is closed under consequence. A way of addressing the second of these is to move from knowledge simpliciter, to knowledge for a reason. Then, as consequences become 'further away' from one's original knowledge, reasons for them become more complex, thus providing a kind of resource measurement. Of course, one kind of reason is a formal proof. In this context, what one gets is a semantics for Artemov's Logic of Proofs (LP), a semantics that can be used to re-establish a number of basic results about LP, but from a different direction. I will present this semantics, and sketch how some of the important facts about LP can be derived using it.
Haim Gaifman
There is a direct route from Cantor's 1891 diagonal construction to the 1934 Goedel-Carnap fixed point theorem, which is also probably how Goedel got the idea of his proof. The route goes on to Kleene's 1938 recursion theorem. When these results are viewed in the right light, they turn out to be special cases of a general theorem, which is phrased in terms of a generalized notion of language and naming. The modeling I shall suggest makes place for uncustomary "languages", and enables a uniform treatment of various results. It also leads to some technical questions, of which I know partial answers. There is a philosophical aspect to all this, concerning the notion of "language" and connections to the Liar paradox.
David Harel
A novel approach to programming reactive systems, that uses live sequence charts (LSCs), is founded upon an inter-object, scenario- based philosophy of behavioral description. While highly intuitive as a programming medium, it raises unusual issues of executability and operational semantics. One of the most novel ideas that this has triggered is "smart" play-out, whereby parts of the execution mechanism are computed in advance using model-checking, and are then simply carried out. Thus, we employ formal verification techniques, themselves based on temporal logic and automata theory, to run programs, not to prove them correct. The talk will also describe our use of play-in/play-out in modeling biological systems, specifically the egg-laying development of the C. elegans nematode.
(Joint work with Hillel Kugler and others)
Zurab Khasidashvili
We present a simple axiomatization of residual relation in conflict-free models of computation, such as Peano arithmetic or the lambda-calculus, originated from work of J.-J. Lévy. When combined with a general, abstract concept of "result of computation", such as head-normal forms or Bohm-trees in the lambda-calculus, the axiomatization allows us to prove the normalization and optimality results in a very general form. Further, we can define an event-structure style semantics for conflict-free computation in general (where redexes can be replicated or erased), and formalize a concept of "modularity" or "independence" of computation, allowing us to build Euclid-like Geometry of Reduction Spaces, supporting a concept of "decomposition" of computation with respect to a basis. Finally, we show how the axiomatization of residuals can be translated into partial orders more directly, in the spirit of Kahn & Plotkin's work on concrete domains, yielding a concept of partial orders that can capture duplication of redexes during computation.
(Joint work with John Glauert)
Danny Lehmann
Intriguing links have recently been discovered between the logic of Quantum measurements and the non-monotonic logics developed in Artificial Intelligence to model jumping to conclusions on the basis of less than totally conclusive evidence.
Zohar Manna
We describe methods for proving termination. We present a
method for handling linear systems that display non-linear behavior.
Alex Rabinovich
The objectives are to survey classical and recent expressive completeness results and to provide some external yardsticks by which the expressive power of temporal logics can be measured.
Mooly Sagiv
We provide a parametric framework for verifying properties of concurrent Java programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to error-detection algorithms that are more precise than existing techniques. The framework also provides the most precise shape-analysis algorithm for concurrent programs. In contrast to existing verification techniques, we do not put a bound on the number of allocated objects. The framework even produces interesting results when analyzing Java programs with an unbounded number of threads.
A prototype of the framework has been implemented using TVLA (http://www.math.tau.ac.il/~rumster/TVLA).
This work is part of Ph.D. of Eran Yahav (http://www.cs.tau.ac.il/~yahave).
Vladimir Sazonov
Since 1970, when E.F. Codd introduced the relational approach to databases, Relational Databases have become the mainstream both in database theory and in the industry of database management systems. This is one of the brightest examples of the influence of mathematics and mathematical logic (where relation is also a fundamental concept) on computer practice. Now a new idea of semistructured databases (SSD) has arisen. It does not fit well with the relational approach although it is usually presented in terms of edge labelled graphs which are mathematically just two column relational tables (with labelled rows). The point is that some other kind of issues with such graphs arises which are not so "relational".
The Hyperset approach to SSD is intimately connected with the graph approach and is, in fact, a natural generalization of the relational approach. The idea is extremely simple, but abstract. Each vertex X of a graph is considered as a (hyper)set name and generates a set equation X = {l_1:X_1,...,l_n:X_n} where l_i:X -> X_i are all outgoing l_i-labelled edges. According to the (non-wellfounded) Hyperset Theory (from a book of P.Azcel or another book of J. Barwise and L. Moss) each such system of set equations generated by a graph has a unique solution in the universe of (abstract) hypersets. Each hyperset X is a set of labelled sets of sets of sets, etc., possibly with cycles (according to the given graph or system of set equations). Thus, graph vertices only represent hypersets. These are hypersets which are considered as (abstract) SSD states (like relations which are also sets of tuples). Any query to SSD in this approach is just an operation over hypersets (like operations over relations in the relational approach to databases), whereas graphs or, equivalently, systems of set equations representing hypersets and SSDs serve to compute these abstract operations/queries by appropriate (restructuring and bisimulation invariant) graph transformers.
A hyperset query language Delta and its more practical version will be discussed whose expressive power proves to be exactly PTIME (also for the case of multi-hypersets). Some variations of Delta for the case of acyclic graphs (sets) have expressive power (N/D)LOGSPACE. No such results are known to the author for purely graph approaches to SSD (without involving hypersets). Any SSD, as a system of hyperset equations, may be divided into parts and represented as, say, HTML files distributed potentially over the world with each set name X_i "clickable" and leading to (either the same or possibly remote) file with the corresponding equation X_i = {...}. This, as well as the arbitrary graph structure of SSD, suggests calling such databases Web-like (WDB). Thus, in principle, the Delta-language can be considered as a powerful, flexible and restructuring (unlike the usual querying mechanisms of, e.g., Google) query language to WDB or even to WWW.
Some implementation issues potentially leading to a WDBMS, (like many existing RDBMS) for example, multiple mobile distributed agent execution of Delta queries may be discussed, too.
(This talk is based on joint works with my colleagues Alexei Lisitsa, Alexandr Leontjev and Yuri Serdyuk. Also, student Richard Molyneux is currently working on a new attempt of implementation of Delta based on HTML files of the above kind.)
Eli Shamir
Conjunctive/disjunctive forms[CNF/DNF] can express any function, but excessive length and non-unique representation are drawbacks compared to circuits, BDDs. However satisfaction/refutation look simpler since ONE clause, or All clauses are involved. Algorithms to refute f [plus providing a counterexample] are fundamental in formal verification of designs. Difficulties grow when the formula size is near the "sharp threshold" on length(f), where the satisfying set R(f) becomes empty "almost surely". Physicists study the topology of this R, using spin glass analogies. We concentrate on the size |R| as a function of length(f). For clause size k growing slowly with n [number of variables], our results give a rather full picture-relying on a "pseudo-random" structure condition: two clauses have only few variables in common. It is instructive to see how it implies uniqueness of representation and also learning algorithms reconstructing THE clauses of f from random examples. Cases of fixed clause size [k>=3] are notorious for their threshold-related difficulty, and many studies produced partial/heuristic results. It becomes even worse for the size of R: even the case k=2 is open, not clear if Fridgut technique helps. We give some results explaining why this is so.
Anatol Slissenko
The purpose of this talk is to discuss some results, open questions and possible approaches to the development efficient decidability algorithms for verification in the framework of predicate logics with explicit time. The application domain is (timed) distributed algorithms, in particular, cryptographic protocols.
Mars K. Valiev
We consider the problem of verifying dynamic (temporal) properties for multi-agent systems (MA-systems) consisting of interacting program agents with intellectual components. Such systems represent one of the most actively developing areas in the modern software engineering and artificial intelligence, and became especially popular with development of Internet technologies.
In the model of the MA-systems which we consider, states of agents are described by sets of facts (analogues of local relational databases), the intellectual components are described by logical programs with updates of the states, and interaction of agents is performed through mailboxes. The model follows lines of MA- systems with the IMPACT architecture introduced by V.S. Subrahmanian et al., but is conceptually simpler and moreconvenient for the theoretical investigation.
We define deterministic, nondeterministic and asynchronous versions of operational semantics for the MA-systems. It is clear that verifying some rather simple dynamic properties is undecidable for the general logic programs which can work with infinite state spaces. To exclude this we introduce some natural restrictions on intellectual components of agents which make all systems we consider, finite-state.
The dynamical properties of the deterministic MA-systems are natural to describe in some variants of the first-order logic of linear time, and the properties of nondeterministic and asynchronous MA-systems in the first-order logic of branching time or in the first- order temporal mu-calculus.
It is clear that verifying these properties for the (finite-state) MA- systems is decidable. But in the most general case of verifying formulas of mu-calculus on nonground nondeterministic or asynchronous MA-systems the time complexity is very high: nondeterministic double exponential. Our main results are connected with establishing some tight bounds on complexity of the problem for restricted classes of MA-systems. In some cases of these restrictins we have deterministic or nondeterministic polynomial time complexity, in other - completeness in EXPTIME, and so on.
(Joint work with M. I. Dekhtyar, A. Ja. Dikovsky)