On the relative complexity of labelled modal tableaux

We investigate the relative complexity of two free-variable labelled modal tableaux(KEM and Single Step Tableaux, SST). We discuss the reasons why p-simulation is not a proper measure of the relative complexity of tableaux-like proof systems, and we propose an improved comparison scale (p-search-simulation). Finally we show that KEM p-search-simulates SST while SST cannot p-search-simulate KEM.

Labelled tableaux for non-normal modal logics

In this paper we show how to extend KEM, a tableau-like proof system for normal modal logic, in order to deal with classes of non-normal modal logics, such as monotonic and regular, in a uniform and modular way.

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.

Aplicación de los Tableaux analíticos para la determinación de las relaciones de accesibilidad en Marcos de Kripke para la Lógica Modal Proposicional

Fil: Durán, Cecilia. Universidad Nacional de La Plata. Facultad de Humanidades y Ciencias de la Educación; Argentina.

Approximations of modal logics: K and beyond

Inspired by the recent work on approximations of classical logic, we present a method that approximates several modal logics in a modular way. Our starting point is the limitation of the n-degree of introspection that is allowed, thus generating modal n-logics. The semantics for n-logics is presented, in which formulas are evaluated with respect to paths, and not possible worlds. A tableau-based proof system is presented, n-SST, and soundness and completeness is shown for the approximation of modal logics K, T, D, S4 and S5. (c) 2008 Published by Elsevier B.V.

Proof theory of quantified modal logics

We introduce labelled sequent calculi for indexed modal logics. We prove that the structural rules of weakening and contraction are height-preserving admissible, that all rules are invertible, and that cut is admissible. Then we prove that each calculus introduced is sound and complete with respect to the appropriate class of transition frames.

Modal interpolation via nested sequents

The main method of proving the Craig Interpolation Property (CIP) constructively uses cut-free sequent proof systems. Until now, however, no such method has been known for proving the CIP using more general sequent-like proof formalisms, such as hypersequents, nested sequents, and labelled sequents. In this paper, we start closing this gap by presenting an algorithm for proving the CIP for modal logics by induction on a nested-sequent derivation. This algorithm is applied to all the logics of the so-called modal cube.

Optimization of modal filters based on arrays of piezoelectric sensors

Modal filters may be obtained by a properly designed weighted sum of the output signals of an array of sensors distributed on the host structure. Although several research groups have been interested in techniques for designing and implementing modal filters based on a given array of sensors, the effect of the array topology on the effectiveness of the modal filter has received much less attention. In particular, it is known that some parameters, such as size, shape and location of a sensor, are very important in determining the observability of a vibration mode. Hence, this paper presents a methodology for the topological optimization of an array of sensors in order to maximize the effectiveness of a set of selected modal filters. This is done using a genetic algorithm optimization technique for the selection of 12 piezoceramic sensors from an array of 36 piezoceramic sensors regularly distributed on an aluminum plate, which maximize the filtering performance, over a given frequency range, of a set of modal filters, each one aiming to isolate one of the first vibration modes. The vectors of the weighting coefficients for each modal filter are evaluated using QR decomposition of the complex frequency response function matrix. Results show that the array topology is not very important for lower frequencies but it greatly affects the filter effectiveness for higher frequencies. Therefore, it is possible to improve the effectiveness and frequency range of a set of modal filters by optimizing the topology of an array of sensors. Indeed, using 12 properly located piezoceramic sensors bonded on an aluminum plate it is shown that the frequency range of a set of modal filters may be enlarged by 25-50%.

A contribution to the exact modal solution of in-plane beam structures

The exact vibration modes and natural frequencies of planar structures and mechanisms, comprised Euler-Bernoulli beams, are obtained by solving a transcendental. nonlinear, eigenvalue problem stated by the dynamic stiffness matrix (DSM). To solve this kind of problem, the most employed technique is the Wittrick-Williams algorithm, developed in the early seventies. By formulating a new type of eigenvalue problem, which preserves the internal degrees-of-freedom for all members in the model, the present study offers an alternative to the use of this algorithm. The new proposed eigenvalue problem presents no poles, so the roots of the problem can be found by any suitable iterative numerical method. By avoiding a standard formulation for the DSM, the local mode shapes are directly calculated and any extension to the beam theory can be easily incorporated. It is shown that the method here adopted leads to exact solutions, as confirmed by various examples. Extensions of the formulation are also given, where rotary inertia, end release, skewed edges and rigid offsets are all included. (C) 2008 Elsevier Ltd. All rights reserved.

Non-linear modal analysis for beams subjected to axial loads: Analytical and finite-element solutions

A rigorous derivation of non-linear equations governing the dynamics of an axially loaded beam is given with a clear focus to develop robust low-dimensional models. Two important loading scenarios were considered, where a structure is subjected to a uniformly distributed axial and a thrust force. These loads are to mimic the main forces acting on an offshore riser, for which an analytical methodology has been developed and applied. In particular, non-linear normal modes (NNMs) and non-linear multi-modes (NMMs) have been constructed by using the method of multiple scales. This is to effectively analyse the transversal vibration responses by monitoring the modal responses and mode interactions. The developed analytical models have been crosschecked against the results from FEM simulation. The FEM model having 26 elements and 77 degrees-of-freedom gave similar results as the low-dimensional (one degree-of-freedom) non-linear oscillator, which was developed by constructing a so-called invariant manifold. The comparisons of the dynamical responses were made in terms of time histories, phase portraits and mode shapes. (C) 2008 Elsevier Ltd. All rights reserved.

Modal functions of future tenses in French

The paper disputes two influential claims in the Romance Linguistics literature. The first is that the synthetic future tenses in spoken Western Romance are now rivalled, if not supplanted, as temporal functors by the more recently developed GO futures. The second is that these synthetic futures now have modal rather than temporal meanings in spoken Romance. These claims are seen as reflecting a universal cycle of diachronic change, in which verb forms originally expressing modal (or aspectual) values take on future temporal reference, becoming tenses. The new modal meanings supplant the temporal, which are then taken up by new forms. Challenges to this theory for French are raised on the basis of empirical evidence of two sorts. Positively, future tenses in spoken Romance continue to be used with temporal meaning. Negatively, evidence of modal meaning for these forms is lacking. The evidence comes froma corpora of spoken French, native speaker judgements and verb data from a daily broadsheet. Cumulatively, it points to the reverse of the claims noted above: the synthetic future in spoken French has temporal but little modal meaning.