scholarly journals Revisiting separation: algorithms and complexity

2020 ◽  
Author(s):  
Daniel Oliveira ◽  
João Rasga
Keyword(s):  
Temporal Logic ◽  
Linear Orders ◽  
Boolean Combination ◽  
First Order ◽  
The Past ◽  
Double Exponential ◽  
Algorithms And Complexity ◽  
Size Growth ◽  
Monadic Logic ◽  
Exponential Size

Abstract Linear temporal logic (LTL) with Since and Until modalities is expressively equivalent, over the class of complete linear orders, to a fragment of first-order logic known as FOMLO (first-order monadic logic of order). It turns out that LTL, under some basic assumptions, is expressively complete if and only if it has the property, called separation, that every formula is equivalent to a Boolean combination of formulas that each refer only to the past, present or future. Herein we present simple algorithms and their implementations to perform separation of the LTL with Since and Until, over discrete and complete linear orders, and translation from FOMLO formulas into equivalent temporal logic formulas. We additionally show that the separation of a certain fragment of LTL results in at most a double exponential size growth.

scholarly journals “Most of” leads to undecidability: Failure of adding frequencies to LTL

2021 ◽  
pp. 82-101
Author(s):  
Bartosz Bednarczyk ◽  
Jakub Michaliszyn
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Statistical Reasoning ◽  
First Order ◽  
High Interest ◽  
The Past ◽  
Influence Networks

AbstractLinear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that $$\sigma $$ σ is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and discuss how the undecidability results transfer to first-order logic on words.

scholarly journals First-Order Logic with Two Variables and Unary Temporal Logic

1997 ◽  
Vol 4 (5) ◽  
Author(s):  
Kousha Etessami ◽  
Moshe Y. Vardi ◽  
Thomas Wilke
Keyword(s):  
Computational Complexity ◽  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Model Property ◽  
First Order ◽  
The Past ◽  
Small Model ◽  
Input Formula

We investigate the power of first-order logic with only two variables over<br />omega-words and finite words, a logic denoted by FO2. We prove that FO2 can<br />express precisely the same properties as linear temporal logic with only the unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, a logic we denote by unary-TL. Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is optimal.<br />While satisfiability for full linear temporal logic, as well as for<br />unary-TL, is known to be PSPACE-complete, we prove that satisfiability<br />for FO2 is NEXP-complete, in sharp contrast to the fact that satisfiability<br />for FO3 has non-elementary computational complexity. Our NEXP time<br />upper bound for FO2 satisfiability has the advantage of being in terms of<br />the quantifier depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely: a satisfiable FO2 formula has a model whose “size” is at most exponential in the quantifier depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.

scholarly journals Mathematical Creativity in Adults: Its Measurement and Its Relation to Intelligence, Mathematical Competence and General Creativity

2021 ◽  
Vol 9 (1) ◽  
pp. 10
Author(s):  
Michaela A. Meier ◽  
Julia A. Burgstaller ◽  
Mathias Benedek ◽  
Stephan E. Vogel ◽  
Roland H. Grabner
Keyword(s):  
Exploratory Study ◽  
Mathematical Creativity ◽  
Good Reliability ◽  
Mathematical Competence ◽  
First Order ◽  
The Past ◽  
Confirmatory Factor ◽  
Order Factor ◽  
General Creativity ◽  
Creativity Measure

Mathematical creativity is perceived as an increasingly important aspect of everyday life and, consequently, research has increased over the past decade. However, mathematical creativity has mainly been investigated in children and adolescents so far. Therefore, the first goal of the current study was to develop a mathematical creativity measure for adults (MathCrea) and to evaluate its reliability and construct validity in a sample of 100 adults. The second goal was to investigate how mathematical creativity is related to intelligence, mathematical competence, and general creativity. The MathCrea showed good reliability, and confirmatory factor analysis confirmed that the data fitted the assumed theoretical model, in which fluency, flexibility, and originality constitute first order factors and mathematical creativity a second order factor. Even though intelligence, mathematical competence, and general creativity were positively related to mathematical creativity, only numerical intelligence and general creativity predicted unique variance of mathematical creativity. Additional analyses separating quantitative and qualitative aspects of mathematical creativity revealed differential relationships to intelligence components and general creativity. This exploratory study provides first evidence that intelligence and general creativity are important predictors for mathematical creativity in adults, whereas mathematical competence seems to be not as important for mathematical creativity in adults as in children.

Old and New Results for First Order Periodic ODEs without Uniqueness: a Comprehensive Study by Lower and Upper Solutions

2004 ◽  
Vol 4 (3) ◽  
Author(s):  
Franco Obersnel ◽  
Pierpaolo Omari
Keyword(s):  
Cauchy Problem ◽  
Differential Equations ◽  
Lower And Upper Solutions ◽  
Elementary Approach ◽  
Qualitative Properties ◽  
First Order ◽  
The Past ◽  
The Cauchy Problem ◽  
Qualitative Properties Of Solutions ◽  
Comprehensive Study

AbstractAn elementary approach, based on a systematic use of lower and upper solutions, is employed to detect the qualitative properties of solutions of first order scalar periodic ordinary differential equations. This study is carried out in the Carathéodory setting, avoiding any uniqueness assumption, in the future or in the past, for the Cauchy problem. Various classical and recent results are recovered and generalized.

scholarly journals Memory and reflection

2021 ◽  
Vol 44 (spe2) ◽  
pp. 151-168
Author(s):  
Chienkuo Mi
Keyword(s):  
Problem Solving ◽  
Virtue Epistemology ◽  
Animal Cognition ◽  
Active Role ◽  
Careful Examination ◽  
First Order ◽  
The Past ◽  
The Analects ◽  
Normative Status ◽  
Previous Learning

Abstract: I have argued that the Analects of Confucius presents us with a conception of reflection with two components, a retrospective component and a perspective component. The former component involves hindsight or careful examination of the past and as such draws on previous learning or memory and previously formed beliefs to avoid error. The latter component is foresight, or forward looking, and as such looks to existing beliefs and factors in order to achieve knowledge. In this paper, I raise the problem of forgetting and argue that most of contemporary theories of knowledge have to face the problem and deal with the challenge seriously. In order to solve the problem, I suggest a bi-level virtue epistemology which can provide us with the best outlook for the problem-solving. I will correlate two different cognitive capacities or processes of “memory” (and “forgetting”) with the conception of reflection, and evaluate them under two different frameworks, a strict deontic framework (one that presupposes free and intentional determination) and a more loosely deontic framework (one that highlights functional and mechanical faculties). The purpose is to show that reflection as meta-cognition plays an important and active role and enjoys a better epistemic (normative) status in our human endeavors (cognitive or epistemic) than those of first-order (or animal) cognition, such as memory, can play.

scholarly journals THE TIME CAPSULE IN THE POST-SOVIET SOVKHOZ

2020 ◽  
Vol 16 (47) ◽  
pp. 84-110
Author(s):  
Elena Malaya ◽  
Keyword(s):  
Temporal Logic ◽  
Soviet Economy ◽  
Soviet Period ◽  
Historical Time ◽  
State Farm ◽  
The Past ◽  
North East ◽  
The North ◽  
Time Capsule ◽  
Post Soviet Period

The article is devoted to ideas about the Soviet era, widespread in а village in the north-east of Crimea. The paper offers an analysis of how the community, formed around a partially preserved state farm, builds its own picture of historical time, expands the imaginary boundaries of the Soviet period, and also thinks of it not so much as the past, but as the past future. Particular attention is paid to the object that organizes its temporality — а time capsule, which was laid twice in the studied village (in 1967 and in 2017), as well as its connection with the teleology of modernism. The article compares letters to descendants, sealed in two time capsules, as well as additional documents sent to the future. The text of the 1967 letter is based on a progressive narrative and contains a list of economic indicators of the success of the Soviet economy. By contrast, the 2017 text creates a picture of an unstable time of change, in which the focus is not on the predictable future, but on the vague past and present. The author of the article explains the nostalgia for the Soviet era in the studied community by the reaction to the changes and crises of the post-Soviet period, and suggests using temporal logic in the research of post-socialism.

scholarly journals The exponential eigenmodes of the carbon-climate system, and their implications for ratios of responses to forcings

2013 ◽  
Vol 4 (1) ◽  
pp. 31-49 ◽  
Author(s):  
M. R. Raupach
Keyword(s):  
Linear Systems ◽  
Co2 Emissions ◽  
Radiative Forcing ◽  
Co2 Emission ◽  
Climate Model ◽  
Climate System ◽  
First Order ◽  
The Past ◽  
Emissions Scenarios ◽  
Co2 Sink

Abstract. Several basic ratios of responses to forcings in the carbon-climate system are observed to be relatively steady. Examples include the CO2 airborne fraction (the fraction of the total anthropogenic CO2 emission flux that accumulates in the atmosphere) and the ratio T/QE of warming (T) to cumulative total CO2 emissions (QE). This paper explores the reason for such near-constancy in the past, and its likely limitations in future. The contemporary carbon-climate system is often approximated as a set of first-order linear systems, for example in response-function descriptions. All such linear systems have exponential eigenfunctions in time (an eigenfunction being one that, if applied to the system as a forcing, produces a response of the same shape). This implies that, if the carbon-climate system is idealised as a linear system (Lin) forced by exponentially growing CO2 emissions (Exp), then all ratios of responses to forcings are constant. Important cases are the CO2 airborne fraction (AF), the cumulative airborne fraction (CAF), other CO2 partition fractions and cumulative partition fractions into land and ocean stores, the CO2 sink uptake rate (kS, the combined land and ocean CO2 sink flux per unit excess atmospheric CO2), and the ratio T/QE. Further, the AF and the CAF are equal. Since the Lin and Exp idealisations apply approximately to the carbon-climate system over the past two centuries, the theory explains the observed near-constancy of the AF, CAF and T/QE in this period. A nonlinear carbon-climate model is used to explore how future breakdown of both the Lin and Exp idealisations will cause the AF, CAF and kS to depart significantly from constancy, in ways that depend on CO2 emissions scenarios. However, T/QE remains approximately constant in typical scenarios, because of compensating interactions between CO2 emissions trajectories, carbon-climate nonlinearities (in land–air and ocean–air carbon exchanges and CO2 radiative forcing), and emissions trajectories for non-CO2 gases. This theory establishes a basis for the widely assumed proportionality between T and QE, and identifies the limits of this relationship.

Small substructures and decidability issues for first-order logic with two variables

2012 ◽  
Vol 77 (3) ◽  
pp. 729-765 ◽  
Author(s):  
Emanuel Kieroński ◽  
Martin Otto
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Equivalence Relations ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
Surrounding Structure ◽  
Small Model ◽  
Exponential Size

AbstractWe study first-order logic with two variables FO2 and establish a small substructure property. Similar to the small model property for FO2 we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO2 under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO2 has the finite model property and is complete for non-deterministic exponential time, just as for plain FO2. With two equivalence relations, FO2 does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO2 is undecidable.

Sign in / Sign up

Export Citation Format

Share Document