Eliminability of cut in hypersequent calculi for some modal logics of linear frames

Hypersequent calculi, introduced independently by Pottinger and Avron, provide a powerful generalization of ordinary sequent calculi. In the paper we present a proof of eliminability of cut in hypersequent calculi for three modal logics of linear frames: K4.3, KD4.3 and S4.3. Our cut-free calculus is based on Avron's HC formalization for Gödel–Dummett's logic. The presented proof of eliminability of cut is purely syntactical and based on Ciabattoni, Metcalfe, Montagna's proof of eliminability of cut for hypersequent calculi for some fuzzy logics with modalities.     

Logic of Proofs and Labels with a Complete Set of Operations

We develop a framework in which operations on proofs can bespecified and studied. Proofs are treated as structures builtfrom atomic proofs and references by means of computable operations. Our approach extends the ideas of Logic of Proofs (Artemov,1995, Bull. Symb. Logic, 7, 1–36) in which the proof predicate‘t is a proof of F ’ is incorporated into the propositionallanguage. We introduce an additional storage predicate ‘xis a label for F ’ (Yavorskaya, 2005, J. Logic Comput.,15, 517–537). In this article which is essentially a continuation of Yavorskaya'swork, we study a natural example of a logic with operationson proofs and labels. This logic is decidable and complete with respect to its intended semantics. is capable to internalizeits own proofs, and operations of suffice to realize all operations specified in the languagewith proofs and labels.     

Fixpoint and While Temporal Query Languages

The article investigates the expressive power of implicit temporalquery languages. These languages are designed while assumingtemporal data modelled as sequences of data. So far, two stylesof implicit temporal query languages are known: T-WHILE likelanguages are based on a temporal extension of WHILE with leftand right moves; µTL like languages are a fixpoint extensionof TL. This article focusses on comparing the expressive powerof T-WHILE style languages and µTL languages and providescomplementary results with respect to Abiteboul et al. (1999,J. Comput. System Sci.,58, 54–68). The main contributionis the proof of the equivalence of the three following temporallanguages: the non-inflationary variant of µTL, the languageT-WHILE and more surprisingly the language T-FIXPOINT.     

Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic

There has been a great deal of work on characterizing the complexityof the satisfiability and validity problem for modal logics.In particular, Ladner showed that the satisfiability problemfor all logics between K and S4 is PSPACE-hard, while for S5it is NP-complete. We show that it is negative introspection,the axiom ¬K_p K¬K_p, that causes the gap: if we addthis axiom to any modal logic between K and S4, then the satisfiabilityproblem becomes NP-complete. Indeed, the satisfiability problemis NP-complete for any modal logic that includes the negativeintrospection axiom.     

Computability in Specification

In reference (Foundation of specification. Journal of Logicand Computation, 15, 951–974, 2005), the author introducesa core specification theory (CST) in order to provide a logicalframework for the design and exploration of specification languages.In this article, we formulate two highly expressive extensionsof CST. The first (CST_U) is CST + a universe of types and thesecond (CST_US) permits specifications themselves to be dataitems. Finally, we shall explore their metamathematical propertiesand, in particular, provide an interpretation into first-orderarithmetic.     

Coloured Petri net refinement specification and correctness proof with Coq

In this work, we address the issue of the formal proof (using the proof assistant Coq) of refinement correctness for symmetric nets, a subclass of coloured Petri nets. We provide a formalisation of the net models, and of their type refinement in Coq. Then the Coq proof assistant is used to prove the refinement correctness lemma. An example adapted from a protocol example illustrates our work.     

On Action Logic: Equational Theories of Action Algebras

Pratt (1991, Proceedings of JELIA’90, Volume 478, pp.97–120) defines action algebras as Kleene algebras withresiduals and action logic as the equational theory of actionalgebras. In contrast to Kleene algebras, action algebras forma (finitely based) variety. Jipsen (2004, Studia Logica, 76,291–303) proposes a Gentzen-style sequent system for actionlogic but leaves it as an open question if this system admitscut-elimination and if action logic is decidable. We show thatJipsen's system does not admit cut-elimination. We prove thatthe equational theory of *-continuous action algebras and thesimple Horn theory of *-continuous Kleene algebras are not recursivelyenumerable and they possess FMP, but action logic does not possessFMP.     

Analytic Calculi for Logics of Ordinal Multiples of Standard t-Norms

For two propositional fuzzy logics, we present analytic proofcalculi, based on relational hypersequents. The logic consideredfirst, called M, is based on the finite ordinal sums of ukasiewiczt-norms. In addition to the usual connectives—the conjunction, the implication and the constant 0—we use a furtherunary connective interpreted by the function associating witheach truth value a the greatest -idempotent below a. M is aconservative extension of Basic Logic. The second logic, called M, is based on the finite ordinal sumsof the product t-norm on (0, 1]. Our connectives are in thiscase just the conjunction and the implication.     

On Reduction Systems Equivalent to the Non-associative Lambek Calculus with the Empty String

The article concludes a series of results on cut-rule axiomatizabilityof the Lambek calculus. It is proved that the non-associativeproduct-free Lambek calculus with the empty string (NL₀) isnot finitely axiomatizable if the only rule of inference admittedis Lambek's cut rule. The proof makes use of the (infinitely)cut-rule axiomatized calculus NC designed by the author exactlyfor that purpose.     

Epistemic Actions as Resources

We provide an algebraic semantics together with a sound andcomplete sequent calculus for information update due to epistemicactions. This semantics is flexible enough to accommodate incompleteas well as wrong information e.g. due to secrecy and deceit,as well as nested knowledge. We give a purely algebraic treatmentof the muddy children puzzle, which moreover extends to situationswhere the children are allowed to lie and cheat. Epistemic actions,that is, information exchanges between agents , are modeled as elements of a quantale. The quantale acts on an underlying Q-rightmodule of epistemic propositions and facts. The epistemic content is encoded by appearance maps,one pair and of (lax) morphisms for each agent , which preserve the module and quantale structurerespectively. By adjunction, they give rise to epistemic modalities,capturing the agents' knowledge on propositions and actions.The module action is epistemic update and gives rise to dynamicmodalities—cf. weakest precondition. This model subsumesthe crucial fragment of Baltag, Moss and Solecki's dynamic epistemiclogic, abstracting it in a constructive fashion while introducingresource-sensitive structure on the epistemic actions.     

Isolation, Infima and Diamond Embeddings

In (1993, Annals of Pure and Applied Logic, 62, 207–263),Kaddah pointed out that there are two d.c.e. degrees a,b forminga minimal pair in the d.c.e. degrees, but not in the degrees. Kaddah's; result shows thatLachlan's; theorem, stating that the infima of two c.e. degreesin the c.e. degrees and in the degrees coincide, cannot be generalized to the d.c.e. degrees. In this article, we apply Kaddah's; idea to show that thereare two d.c.e. degrees c,d such that c cups d to 0', and capsd to 0 in the d.c.e. degrees, but not in the degrees. As a consequence, the diamond embedding{0,c,d,0'} is different from the one first constructed by Downeyin 1989 in [5]. To obtain this, we will construct c.e. degreesa,b, d.c.e. degrees c > a,d > b and a non-zero -c.e. degreee c,d such that (i) a,b form a minimal pair, (ii) a isolatesc, and (iii) b isolates d. From this, we can have that c,d forma minimal pair in the d.c.e. degrees, and Kaddah's; result followsimmediately. In our construction, we apply Kaddah's; originalidea to make e below both c and d. Our construction allows usto separate the minimal pair argument (ab = 0), the splittingof 0' (cd = 0'), and the non-minimal pair of c,d (in the degrees), into several parts, to avoiddirect conflicts that could be involved if only c,d and e areconstructed. We also point out that our construction allowsus to make a,b above (and hence c,d) high.     

Stream processing coalgebraically

We study various operations for splitting, partitioning, projecting and merging streams of data. These operations are motivated by their use in dataflow programming and stream processing languages. We use the framework of stream calculus and stream circuits for defining and proving properties of such operations using behavioural differential equations and coinduction proof principles. As a featured example we give proofs of results, observed by Moessner, from elementary number theory using our framework. We study the invariance of certain well patterned classes of streams, namely rational and algebraic streams, under splitting and merging. Finally we show that stream circuits extended with gates for dyadic split and merge are expressive enough to realise some non-rational algebraic streams, thereby going beyond ordinary stream circuits.     

A note on standard completeness for some extensions of uninorm logic

We prove standard completeness for uninorm logic extended with knotted axioms. This is done following a proof-theoretical approach, based on the elimination of the density rule in suitable hypersequent calculi.     

Proof Complexity of the Cut-free Calculus of Structures

We investigate the proof complexity of analytic subsystems ofthe deep inference proof system SKSg (the calculus of structures).Exploiting the fact that the cut rule (i) of SKSg correspondsto the ¬-left rule in the sequent calculus, we establishthat the ‘analytic'system KSg+c has essentially the samecomplexity as the monotone Gentzen calculus MLK. In particular,KSg+c quasipolynomially simulates SKSg, and admits polynomial-sizeproofs of some variants of the pigeonhole principle.     

A Semantic Proof of Polytime Soundness of Light Affine Logic

We define realizability semantics for Light Affine Logic ( LAL\mathsf{LAL} ) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-soundness of LAL\mathsf{LAL} which is considerably simpler than the standard proof based on proof nets and is entirely semantical in nature. The model construction uses a new instance of a resource monoid; a general method for interpreting systems based on Linear Logic introduced earlier by the authors.     

A timed calculus for wireless systems

We propose a timed broadcasting process calculus for wireless systems where time-consuming communications are exposed to collisions. The operational semantics of our calculus is given in terms of a labelled transition system. The calculus enjoys a number of desirable time properties such as (i) time determinism: the passage of time is deterministic; (ii) patience: devices will wait indefinitely until they can communicate; (iii) maximal progress: data transmissions cannot be delayed, they must occur as soon as a possibility for communication arises. We use our calculus to model and study MAC-layer protocols with a special emphasis on collisions and security. The main behavioural equality of our calculus is a timed variant of barbed congruence, a standard branching-time and contextually-defined program equivalence. As an efficient proof method for timed barbed congruence we define a labelled bisimilarity. We then apply our bisimulation proof-technique to prove a number of algebraic laws.     

Linear logic by levels and bounded time complexity

We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard’s seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indices, which allows us to extend Girard’s systems while keeping the same complexity properties. In particular, it turns out that Girard’s systems can be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for developing lambda-calculus type assignment systems with more efficient typing algorithms than existing ones.     

Decidability and complexity of Petri nets with unordered data

We prove several decidability and undecidability results for ν-PN, an extension of P/T nets with pure name creation and name management. We give a simple proof of undecidability of reachability, by reducing reachability in nets with inhibitor arcs to it. Thus, the expressive power of ν-PN strictly surpasses that of P/T nets. We encode ν-PN into Petri Data Nets, so that coverability, termination and boundedness are decidable. Moreover, we obtain Ackermann-hardness results for all our decidable decision problems. Then we consider two properties, width-boundedness and depth-boundedness, that factorize boundedness. Width-boundedness has already been proven to be decidable. Here we prove that its complexity is also non-primitive recursive. Then we prove undecidability of depth-boundedness. Finally, we prove that the corresponding “place version” of all the boundedness problems is undecidable for ν-PN. These results carry over to Petri Data Nets.