Search

There is not abstract.

There is not abstract.

The present paper deals with efficiency improvement of backward proof-search of sequents of propositional linear temporal logic, using a loop-type sequent calculus. The improvement is achieved by syntactic transformation of sequents into equivalent to them simpler ones. It is proved that some formulas can be removed from sequents with no impact on their derivability.

Abstract Background There is still insufficient knowledge on the potential effect of mild to moderate sleep-disordered breathing (SDB) that is widely prevalent, often asymptomatic, and largely undiagnosed in patients with stable coronary artery disease (CAD). SDB affects 34% of men and 17% of women aged between 30 and 70. The objective of this study was to evaluate the association between SDB and left ventricular (LV) hypertrophy as well as structural remodeling in stable CAD patients. Methods The study was based on a cross-sectional design. Echocardiography and polysomnography was performed in 772 patients with CAD and with untreated sleep apnea. All study participants underwent testing by Epworth Sleepiness Scale questionnaire. Their mean age, NYHA and left ventricular ejection fraction were, respectively: 57 ± 9 years, 2.1 ± 0.5 and 51 ± 8%, and 76% were men. Sleep apnea (SA) was defined as an apnea-hypopnea-index (AHI) ≥5 events/h, and, non-SA, as an AHI

Audrius Alonderis,1 Giedrius Varoneckas,1 Nijole Raskauskiene,2 Julija Brozaitiene1 1Laboratory of Clinical Physiology and Rehabilitation, Behavioral Medicine Institute, Lithuanian University of Health Sciences, Palanga, Lithuania; 2Laboratory of Psychosomatic Research, Behavioral Medicine Institute, Lithuanian University of Health Sciences, Palanga, Lithuania Background: Sleep apnea (SA) is increasingly recognized as being important in the prognosis of patients with coronary artery disease (CAD); however, symptoms of SA are not easily identified, and as many as 80% of sufferers remain undiagnosed. Aim: This cross-sectional study investigated the prevalence and predictors of SA that may help to increase the awareness and diagnosis of SA in stable CAD patients. Materials and methods: Polysomnography was performed in 772 medically stable CAD patients with untreated SA recruited from the Clinic of Cardiovascular Rehabilitation. Patients were predominantly male (76%), median age was 58 years (32–81). All subjects completed the Epworth sleepiness scale (ESS). The frequency of all apneas and hypopneas associated with 3% oxygen desaturation is referred to as the apnea–hypopnea index (AHI). Mild-to-severe SA was defined as AHI ≥5/h, moderate-to-severe SA as AHI ≥15/h. Results: AHI was within a range of values that was considered normal or only mildly elevated. The median AHI was 3.4 (interquartile range [IQR 1–9]), and 39% of patients had unrecognized mild-to-severe SA (moderate-to-severe in 14%), which was not higher than other known risk indicators for CAD such as hypertension and obesity (83% and 47%, respectively). These patients did not show sleepiness and the risk-related cut-off score for excessive daily sleepiness was lower than the official for ESS. Conclusion: Hypertension, age, male gender, obesity, ESS ≥6, and left ventricular ejection fraction ≤45% were the best predictors of mild-to-severe SA. While, male gender, age 50–70 years and, mainly, the presence of obesity but not hypertension were clinical predictors for moderate-to-severe SA. In addition, association between mild-to-severe SA and obesity was not evident in women. SA is prevalent comorbidity in the stable CAD patients, especially in its asymptomatic mild form. We suggest that SA should be considered in the secondary prevention protocols for CAD. Keywords: apnea–hypopnea index, AHI, age, CAD, gender differences, sleep apnea

Various types of calculi (Hilbert, Gentzen sequent, resolution calculi, tableaux) for propositional linear temporal logic (PLTL) have been considered in the literature. Cutfree Gentzen-type sequent calculi are convenient tools for backward proof-search search of formulas and sequents. In this paper we present a cut-free Gentzen type sequent calculus for PLTL with the operator

Copyright of Lietuvos Matematikos Rinkinys is the property of Vilnius University and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Knowledge of agents associated to particles of quantum system has been modelled in the paper. Also analysis of formulas and satisfiability in the model have been done.

Brodsky’s coding method for propositional logic is considered in the paper. Based on the sequent calculus, the method allows us to determine whether an arbitrary sequent is derivable in the calculus without constructing proof-search trees. The coding method, presented in the paper, can be used as a decision procedure for propositional logic.

Two sequent calculi for temporal logic of knowledge are presented: one containing invariant-like rule and the other containing looping axioms. Its proved that the calculi are equivalent, sound and complete.

We consider three sequent calculi for propositional linear temporal logic (PLTL) which allow us to formalize the properties of operator “always”. The main new results presented in the paper are: (1) introduction of the calculus with looping axioms; (2) the direct proof that the presented calculi are equivalent; (3) the proof of completeness of the calculi with looping axioms and with invariant-like rule based on completeness of the calculus with the infinitary $\omega$-type rule.

The present study concerns the nondisturbing assessment of cardiovascular oscillations of the carotid artery using a novel skin curvature sensor on the neck. The mechanical oscillations of the skin reflect changes of the artery radius and thus relevant physiological data such as cardiac and respiratory activities, their mutual dependencies, and even changes of blood pressure. The skin curvature sensor is easy to handle and it minimally disturbs the patient, which is relevant for many medical areas such as sleep monitoring. Index Terms--Cardiovascular system, carotid artery, physiological sensors, skin curvature sensor.

A labeled sequent calculus LSC for propositional linear discrete time logic PLTL is introduced. Its sub-calculus LSC−TL is proved to be complete for some class of PLTL sequents.

A sequent calculus with Kripke semantics internalization for a propositional temporal logic with time gaps is introduced. All rules of the calculus are context-free and height-preserving invertible. Structural rules are admissible. The calculus is cut free and is proved to be complete.

In this paper, some loop-check free saturation-like decision procedure is proposed for propositional linear temporal logic (PLTL) with temporal operators “next” and “always”. This saturation procedure terminates when special type sequents are obtained. Properties of PLTL allows us to construct backtracking-free decision procedure without histories and loop-check.

The paper deals with specialization of the antecedent negation loop-rule for the negative implication free fragment of the propositional intuitionistic logic.

In the paper, we define some classes of sequents of the propositional intuitionistic logic. These are classes of primarily and α-primarily reducible sequents. Then we show how derivability of these sequents in a propositional intuitionistic logic sequent calculus LJ0 can be checked by means of a propositional classical logic sequent calculus LK0.

There is not abstract.

There is not abstract.