Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

Caracterização microestrutural e propriedades mecânicas em pinos para transmissão mecânica de aço inoxidável martensítico e pinos fusíveis de latão em chave de alta tensão

Pós-graduação em Engenharia Mecânica - FEB

A syntactic realization theorem for justification logics

Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms \$mathsfd\$, \$mathsft\$, \$mathsfb\$, \$mathsf4\$, and \$mathsf5\$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting's realization merging technique. We further strengthen the realization theorem for \$mathsfKB5\$ and \$mathsfS5\$ by showing that the positive introspection operator is superfluous.

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.

Proof theory for lattice-ordered groups

Proof-theoretic methods are developed and exploited to establish properties of the variety of lattice-ordered groups. In particular, a hypersequent calculus with a cut rule is used to provide an alternative syntactic proof of the generation of the variety by the lattice-ordered group of automorphisms of the real number chain. Completeness is also established for an analytic (cut-free) hypersequent calculus using cut elimination and it is proved that the equational theory of the variety is co-NP complete.

Cut Out By The Middle Man: The Free Speech Implications Of Social Network Blocking and Banning In The EU

This article examines social network users’ legal defences against content removal under the EU and ECHR frameworks, and their implications for the effective exercise of free speech online. A review of the Terms of Use and content moderation policies of two major social network services, Facebook and Twitter, shows that end users are unlikely to have a contractual defence against content removal. Under the EU and ECHR frameworks, they may demand the observance of free speech principles in state-issued blocking orders and their implementation by intermediaries, but cannot invoke this ‘fair balance’ test against the voluntary removal decisions by the social network service. Drawing on practical examples, this article explores the threat to free speech created by this lack of accountability: Firstly, a shift from legislative regulation and formal injunctions to public-private collaborations allows state authorities to influence these ostensibly voluntary policies, thereby circumventing constitutional safeguards. Secondly, even absent state interference, the commercial incentives of social media cannot be guaranteed to coincide with democratic ideals. In light of the blurring of public and private functions in the regulation of social media expression, this article calls for the increased accountability of the social media services towards end users regarding the observance of free speech principles

Analysis of the free vibration of rectangular plates with central cut-outs using the discrete Ritz method

We present an analysis of the free vibration of plates with internal discontinuities due to central cut-outs. A numerical formulation for a basic L-shaped element which is divided into appropriate sub-domains that are dependent upon the location of the cut-out is used as the basic building element. Trial functions formed to satisfy certain boundary conditions are employed to define the transverse deflection of each sub-domain. Mathematical treatments in terms of the continuities in displacement, slope, moment, and higher derivatives between the adjacent sub-domains are enforced at the interconnecting edges. The energy functional results, from the proper assembly of the coupled strain and kinetic energy contributions of each sub-domain, are minimized via the Ritz procedure to extract the vibration frequencies and. mode shapes of the plates. The procedures are demonstrated by considering plates with central cut-outs that are subjected to two types of boundary conditions. (C) 2003 Elsevier Ltd. All rights reserved.

Comparison of 3 accelerometer data reduction approaches, step counts, and 2 self-report measures for estimating physical activity in free-living adults

Background Accelerometers have become one of the most common methods of measuring physical activity (PA). Thus, validity of accelerometer data reduction approaches remains an important research area. Yet, few studies directly compare data reduction approaches and other PA measures in free-living samples. Objective To compare PA estimates provided by 3 accelerometer data reduction approaches, steps, and 2 self-reported estimates: Crouter's 2-regression model, Crouter's refined 2-regression model, the weighted cut-point method adopted in the National Health and Nutrition Examination Survey (NHANES; 2003-2004 and 2005-2006 cycles), steps, IPAQ, and 7-day PA recall. Methods A worksite sample (N = 87) completed online-surveys and wore ActiGraph GT1M accelerometers and pedometers (SW-200) during waking hours for 7 consecutive days. Daily time spent in sedentary, light, moderate, and vigorous intensity activity and percentage of participants meeting PA recommendations were calculated and compared. Results Crouter's 2-regression (161.8 +/- 52.3 minutes/day) and refined 2-regression (137.6 +/- 40.3 minutes/day) models provided significantly higher estimates of moderate and vigorous PA and proportions of those meeting PA recommendations (91% and 92%, respectively) as compared with the NHANES weighted cut-point method (39.5 +/- 20.2 minutes/day, 18%). Differences between other measures were also significant. Conclusions When comparing 3 accelerometer cut-point methods, steps, and self-report measures, estimates of PA participation vary substantially.

Calibration and comparison of accelerometer cut points in preschool children

Objective The present study aimed to develop accelerometer cut points to classify physical activities (PA) by intensity in preschoolers and to investigate discrepancies in PA levels when applying various accelerometer cut points. Methods To calibrate the accelerometer, 18 preschoolers (5.8 +/- 0.4 years) performed eleven structured activities and one free play session while wearing a GT1M ActiGraph accelerometer using 15 s epochs. The structured activities were chosen based on the direct observation system Children's Activity Rating Scale (CARS) while the criterion measure of PA intensity during free play was provided using a second-by-second observation protocol (modified CARS). Receiver Operating Characteristic (ROC) curve analyses were used to determine the accelerometer cut points. To examine the classification differences, accelerometer data of four consecutive days from 114 preschoolers (5.5 +/- 0.3 years) were classified by intensity according to previously published and the newly developed accelerometer cut points. Differences in predicted PA levels were evaluated using repeated measures ANOVA and Chi Square test. Results Cut points were identified at 373 counts/15 s for light (sensitivity: 86%; specificity: 91%; Area under ROC curve: 0.95), 585 counts/15 s for moderate (87%; 82%; 0.91) and 881 counts/15 s for vigorous PA (88%; 91%; 0.94). Further, applying various accelerometer cut points to the same data resulted in statistically and biologically significant differences in PA. Conclusions Accelerometer cut points were developed with good discriminatory power for differentiating between PA levels in preschoolers and the choice of accelerometer cut points can result in large discrepancies.

Defining anthropometric cut-off levels related to metabolic risk in a group of Sri Lankan children

Background: Body mass index (BMI) is widely used as a measure of adiposity. However, currently used cut-off values are not sensitive in diagnosing obesity in South Asian populations. Aim: To define BMI and waist circumference (WC), cut-off values representing percentage fat mass (%FM) associated with adverse health outcomes. Subjects and methods: A cross-sectional descriptive study of 285 5–14 year old Sri Lankan children (56% boys) was carried out. Fat mass (FM) was assessed using the isotope (D2O) dilution technique based on 2C body composition model. BMI and WC cut-off values were defined based on %FM associated with adverse health outcomes. Results: Sri Lankan children had a low fat free mass index (FFMI) and a high fat mass index (FMI). Individuals with the same BMI had %FM distributed over a wide range. Lean body tissue grew very little with advancing age and weight gain was mainly due to increases in body fat. BMI corresponding to 25% in males and 35% in females at 18 years was 19.2 kg/m2 and 19.7 kg/m2, respectively. WC cut-off values for males and females were 68.4 cm and 70.4 cm, respectively. Conclusion: This chart analysis clearly confirms that Sri Lankan children have a high %FM from a young age. With age, more changes occur in FM than in fat free mass (FFM). Although the newly defined BMI and WC cut-off values appear to be quite low, they are comparable to some recent data obtained in similar populations.

Changes in the Levels of Free Amino Acids in Various Regions of Cuscuta during Growth

The angiospermous plant parasite Cuscuta derives reduced carbon and nitrogen compounds primarily from its host. Free amino acids along Cuscuta vines in three zones, viz., 0 to 5 cm, 5 to 15 cm, and 15 to 30 cm, which in a broad sense represent the region of cell division, cell elongation and differentiation and vascular tissue differentiation respectively, were quantitatively estimated. The free amino acid content was the highest in the 0 to 5 cm region and progressively decreased along the posterior regions of the vine. The haustorial region showed the lowest content of free amino acids. In general, the free amino acid content in samples collected at 7 p.m. was found to be higher than that in the samples collected at 7 a.m. Three basic amino acids, histidine, the uncommon amino acid γ-hydroxyarginine, and arginine constituted more than 50% of the total free amino acids in all the zones studied except the haustorial region. Aspartic acid and glutamic acid constituted the major portion in the acidic and neutral fraction of amino acids. Glutamine, asparagine, threonine, and serine were eluted together and occurred in substantial amounts. γ-Hydroxyarginine constituted the largest fraction in the cut end exudate of Cuscuta and presumably appeared to be the major form of transport amino acid. γ-Hydroxyarginine was also a major constituent of the basic amino acids in Cuscuta vines parasitizing host plants from widely separated families, suggesting that this amino acid is a biosynthetic product of the parasite rather than that of the hosts. Also, U-14C arginine was converted to γ-hydroxyarginine by cut Cuscuta vines, suggesting that γ-hydroxyarginine is synthesized de novo from arginine by Cuscuta.

Influence of two photon absorption induced free carriers on coherent polariton and phonon generation in ZnTe crystals

Combination of femtosecond Kerr, two photon absorption, and impulsive stimulated Raman scattering (ISRS) experiments have been carried out to investigate the effect of pulse energy and crystal temperature on the generation of coherent polaritons and phonons in 〈110〉 cut ZnTe single crystals of three different resistivities. We demonstrate that the effect of two photon induced free carriers on the creation of both the polaritons and phonons is largest at 4 K where the free carrier lifetime is enhanced. The temperature dependant ISRS on high and low purity ZnTe crystals allows us to unambiguously assign the phonon mode at 3.5 THz to the longitudinal acoustic mode at X-point in the Brillouin zone, LA(X).

Towards topology-free optimization - An application to turbine internal cooling geometries

The application of automated design optimization to real-world, complex geometry problems is a significant challenge - especially if the topology is not known a priori like in turbine internal cooling. The long term goal of our work is to focus on an end-to-end integration of the whole CFD Process, from solid model through meshing, solving and post-processing to enable this type of design optimization to become viable & practical. In recent papers we have reported the integration of a Level Set based geometry kernel with an octree-based cut- Cartesian mesh generator, RANS flow solver, post-processing & geometry editing all within a single piece of software - and all implemented in parallel with commodity PC clusters as the target. The cut-cells which characterize the approach are eliminated by exporting a body-conformal mesh guided by the underpinning Level Set. This paper extends this work still further with a simple scoping study showing how the basic functionality can be scripted & automated and then used as the basis for automated optimization of a generic gas turbine cooling geometry. Copyright © 2008 by W.N.Dawes.