Proof theory for hybrid(ised) logics

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. In a series of papers this process has been detailed and taken as a basis for a speci cation methodology for recon gurable systems. The present paper extends this work by showing how a proof calculus (in both a Hilbert and a tableau based format) for the hybridised version of a logic can be systematically generated from a proof calculus for the latter. Such developments provide the basis for a complete proof theory for hybrid(ised) logics, and thus pave the way to the development of (dedicated) proof support.

Pseudodifferential operators on Hilbert space riggings with associated psi *-algebras and generalized Hörmander classes

The present thesis is concerned with certain aspects of differential and pseudodifferential operators on infinite dimensional spaces. We aim to generalize classical operator theoretical concepts of pseudodifferential operators on finite dimensional spaces to the infinite dimensional case. At first we summarize some facts about the canonical Gaussian measures on infinite dimensional Hilbert space riggings. Considering the naturally unitary group actions in $L^2(H_-,gamma)$ given by weighted shifts and multiplication with $e^{iSkp{t}{cdot}_0}$ we obtain an unitary equivalence $F$ between them. In this sense $F$ can be considered as an abstract Fourier transform. We show that $F$ coincides with the Fourier-Wiener transform. Using the Fourier-Wiener transform we define pseudodifferential operators in Weyl- and Kohn-Nirenberg form on our Hilbert space rigging. In the case of this Gaussian measure $gamma$ we discuss several possible Laplacians, at first the Ornstein-Uhlenbeck operator and then pseudo-differential operators with negative definite symbol. In the second case, these operators are generators of $L^2_gamma$-sub-Markovian semi-groups and $L^2_gamma$-Dirichlet-forms. In 1992 Gramsch, Ueberberg and Wagner described a construction of generalized Hörmander classes by commutator methods. Following this concept and the classical finite dimensional description of $Psi_{ro,delta}^0$ ($0leqdeltaleqroleq 1$, $delta< 1$) in the $C^*$-algebra $L(L^2)$ by Beals and Cordes we construct in both cases generalized Hörmander classes, which are $Psi^*$-algebras. These classes act on a scale of Sobolev spaces, generated by our Laplacian. In the case of the Ornstein-Uhlenbeck operator, we prove that a large class of continuous pseudodifferential operators considered by Albeverio and Dalecky in 1998 is contained in our generalized Hörmander class. Furthermore, in the case of a Laplacian with negative definite symbol, we develop a symbolic calculus for our operators. We show some Fredholm-criteria for them and prove that these Fredholm-operators are hypoelliptic. Moreover, in the finite dimensional case, using the Gaussian-measure instead of the Lebesgue-measure the index of these Fredholm operators is still given by Fedosov's formula. Considering an infinite dimensional Heisenberg group rigging we discuss the connection of some representations of the Heisenberg group to pseudo-differential operators on infinite dimensional spaces. We use this connections to calculate the spectrum of pseudodifferential operators and to construct generalized Hörmander classes given by smooth elements which are spectrally invariant in $L^2(H_-,gamma)$. Finally, given a topological space $X$ with Borel measure $mu$, a locally compact group $G$ and a representation $B$ of $G$ in the group of all homeomorphisms of $X$, we construct a Borel measure $mu_s$ on $X$ which is invariant under $B(G)$.

A chapter in the theory of linear operators in Hilbert space,

Mode of access: Internet.

Bounds for Fractional Powers of Operators in a Hilbert Space and Constants in Moment Inequalities

Mathematics Subject Classification: 47A56, 47A57,47A63

Hilbert-Smith Conjecture for K - Quasiconformal Groups

MSC 2010: 30C60

A Fibred Tableau Calculus for Modal Logics of Agents

In previous works we showed how to combine propositional multimodal logics using Gabbay's \emph{fibring} methodology. In this paper we extend the above mentioned works by providing a tableau-based proof technique for the combined/fibred logics. To achieve this end we first make a comparison between two types of tableau proof systems, (\emph{graph} $\&$ \emph{path}), with the help of a scenario (The Friend's Puzzle). Having done that we show how to uniformly construct a tableau calculus for the combined logic using Governatori's labelled tableau system \KEM. We conclude with a discussion on \KEM's features.

Quantum mechanics as an approximation to classical mechanics in Hilbert space

Classical mechanics is formulated in complex Hilbert space with the introduction of a commutative product of operators, an antisymmetric bracket and a quasidensity operator that is not positive definite. These are analogues of the star product, the Moyal bracket, and the Wigner function in the phase space formulation of quantum mechanics. Quantum mechanics is then viewed as a limiting form of classical mechanics, as Planck's constant approaches zero, rather than the other way around. The forms of semiquantum approximations to classical mechanics, analogous to semiclassical approximations to quantum mechanics, are indicated.

A refinement calculus for logic programs

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.

Enriched behavioral prediction equation and its impact on structured learning and the dynamic calculus

This theoretical note describes an expansion of the behavioral prediction equation, in line with the greater complexity encountered in models of structured learning theory (R. B. Cattell, 1996a). This presents learning theory with a vector substitute for the simpler scalar quantities by which traditional Pavlovian-Skinnerian models have hitherto been represented. Structured learning can be demonstrated by vector changes across a range of intrapersonal psychological variables (ability, personality, motivation, and state constructs). Its use with motivational dynamic trait measures (R. B. Cattell, 1985) should reveal new theoretical possibilities for scientifically monitoring change processes (dynamic calculus model; R. B. Cattell, 1996b), such as encountered within psycho therapeutic settings (R. B. Cattell, 1987). The enhanced behavioral prediction equation suggests that static conceptualizations of personality structure such as the Big Five model are less than optimal.

Induction in the timed interval calculus

The Timed Interval Calculus, a timed-trace formalism based on set theory, is introduced. It is extended with an induction law and a unit for concatenation, which facilitates the proof of properties over trace histories. The effectiveness of the extended Timed Interval Calculus is demonstrated via a benchmark case study, the mine pump. Specifically, a safety property relating to the operation of a mine shaft is proved, based on an implementation of the mine pump and assumptions about the environment of the mine. (C) 2002 Elsevier Science B.V. All rights reserved.

SHACC: a functional prototyper for a component calculus

Over the last decade component-based software development arose as a promising paradigm to deal with the ever increasing complexity in software design, evolution and reuse. SHACC is a prototyping tool for component-based systems in which components are modelled coinductively as generalized Mealy machines. The prototype is built as a HASKELL library endowed with a graphical user interface developed in Swing

Fractional calculus: a survey of useful formulas

This paper presents a survey of useful, established formulas in Fractional Calculus, systematically collected for reference purposes.

On development of fractional calculus during the last fifty years

Fractional calculus generalizes integer order derivatives and integrals. During the last half century a considerable progress took place in this scientific area. This paper addresses the evolution and establishes an assertive measure of the research development.

Science metrics on fractional calculus development since 1966

During the last fifty years the area of Fractional Calculus verified a considerable progress. This paper analyzes and measures the evolution that occurred since 1966.

Fractional order calculus: basic concepts and engineering applications

The fractional order calculus (FOC) is as old as the integer one although up to recently its application was exclusively in mathematics. Many real systems are better described with FOC differential equations as it is a well-suited tool to analyze problems of fractal dimension, with long-term “memory” and chaotic behavior. Those characteristics have attracted the engineers' interest in the latter years, and now it is a tool used in almost every area of science. This paper introduces the fundamentals of the FOC and some applications in systems' identification, control, mechatronics, and robotics, where it is a promissory research field.