Dijkstra's Interpretation of the Approach to Solving a Problem of Program Correctness
Disjunction in modal description logics.
Domain mu-calculus
The basic framework of domain -calculus was formulated in [39] more than ten years ago. This paper provides an improved formulation of a fragment of the -calculus without function space or powerdomain constructions, and studies some open problems related to this -calculus such as decidability and expressive power. A class of language equations is introduced for encoding -formulas in order to derive results related to decidability and expressive power of non-trivial fragments of the domain -calculus....
Domain mu-calculus
The basic framework of domain μ-calculus was formulated in [39] more than ten years ago. This paper provides an improved formulation of a fragment of the μ-calculus without function space or powerdomain constructions, and studies some open problems related to this μ-calculus such as decidability and expressive power. A class of language equations is introduced for encoding μ-formulas in order to derive results related to decidability and expressive power of non-trivial fragments of the domain...
Étude et implémentation d'un système de déduction pour logique algorithmique
Finite sum-product logic.
Fixpoints, games and the difference hierarchy
Drawing on an analogy with temporal fixpoint logic, we relate the arithmetic fixpoint definable sets to the winning positions of certain games, namely games whose winning conditions lie in the difference hierarchy over . This both provides a simple characterization of the fixpoint hierarchy, and refines existing results on the power of the game quantifier in descriptive set theory. We raise the problem of transfinite fixpoint hierarchies.
Fixpoints, games and the difference hierarchy
Drawing on an analogy with temporal fixpoint logic, we relate the arithmetic fixpoint definable sets to the winning positions of certain games, namely games whose winning conditions lie in the difference hierarchy over . This both provides a simple characterization of the fixpoint hierarchy, and refines existing results on the power of the game quantifier in descriptive set theory. We raise the problem of transfinite fixpoint hierarchies.
Formal Specifications in Software Development: an Overview
How to generalize logic programming to arbitrary set of clauses.
Idealized coinductive type systems for imperative object-oriented programs
In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on abstract compilation of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by considering a natural translation of Static Single Assignment intermediate form programs into Horn formulas,...
Idealized coinductive type systems for imperative object-oriented programs
In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on abstract compilation of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by considering a natural translation of Static Single Assignment intermediate form programs into Horn formulas,...
Indexed categories for program development
Many-sorted coalgebraic modal logic : a model-theoretic study
This paper gives a semantical underpinning for a many-sorted modal logic associated with certain dynamical systems, like transition systems, automata or classes in object-oriented languages. These systems will be described as coalgebras of so-called polynomial functors, built up from constants and identities, using products, coproducts and powersets. The semantical account involves Boolean algebras with operators indexed by polynomial functors, called MBAOs, for Many-sorted Boolean Algebras with...
Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study
This paper gives a semantical underpinning for a many-sorted modal logic associated with certain dynamical systems, like transition systems, automata or classes in object-oriented languages. These systems will be described as coalgebras of so-called polynomial functors, built up from constants and identities, using products, coproducts and powersets. The semantical account involves Boolean algebras with operators indexed by polynomial functors, called MBAOs, for Many-sorted Boolean Algebras with...
Map genus, forbidden maps, and monadic second-order logic.
On characteristic formulae for Event-Recording Automata
A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that...
On Core XPath with Inflationary Fixed Points
We prove the undecidability of Core XPath 1.0 (CXP) [G. Gottlob and C. Koch, in Proc. of 17th Ann. IEEE Symp. on Logic in Computer Science, LICS ’02 (Copenhagen, July 2002). IEEE CS Press (2002) 189–202.] extended with an Inflationary Fixed Point (IFP) operator. More specifically, we prove that the satisfiability problem of this language is undecidable. In fact, the fragment of CXP+IFP containing only the self and descendant axes is already undecidable.
On Semantics of a Term Calculus for Classical Logic
On the categorical semantics of elementary linear logic.