scholarly journals Cut Elimination Theorem for Non-Commutative Hypersequent Calculus

2017 ◽  
Vol 46 (1/2) ◽  
Author(s):  
Andrzej Indrzejczak
Keyword(s):  
Temporal Logic ◽  
Cut Elimination ◽  
Temporal Logics ◽  
Hypersequent Calculi ◽  
Flow Of Time

Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.

CUT ELIMINATION IN HYPERSEQUENT CALCULUS FOR SOME LOGICS OF LINEAR TIME

2019 ◽  
Vol 12 (4) ◽  
pp. 806-822
Author(s):  
ANDRZEJ INDRZEJCZAK
Keyword(s):  
Distinctive Feature ◽  
Linear Time ◽  
Cut Elimination ◽  
Temporal Logics ◽  
Flow Of Time ◽  
Equivalent Variant

AbstractThis is a sequel article to [10] where a hypersequent calculus (HC) for some temporal logics of linear frames including Kt4.3 and its extensions for dense and serial flow of time was investigated in detail. A distinctive feature of this approach is that hypersequents are noncommutative, i.e., they are finite lists of sequents in contrast to other hypersequent approaches using sets or multisets. Such a system in [10] was proved to be cut-free HC formalization of respective logics by means of semantical argument. In this article we present an equivalent variant of this calculus for which a constructive syntactical proof of cut elimination is provided.

scholarly journals The temporal logic of coalgebras via Galois algebras

2002 ◽  
Vol 12 (6) ◽  
pp. 875-903 ◽  
Author(s):  
BART JACOBS
Keyword(s):  
State Space ◽  
Temporal Logic ◽  
Metric Spaces ◽  
Linear Temporal Logic ◽  
The State ◽  
Temporal Logics ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Polynomial Functors

This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.

scholarly journals Temporal Logics Over Finite Traces with Uncertainty

2020 ◽  
Vol 34 (06) ◽  
pp. 10218-10225 ◽  
Author(s):  
Fabrizio M Maggi ◽  
Marco Montali ◽  
Rafael Peñaloza
Keyword(s):  
Decision Making ◽  
Temporal Logic ◽  
Business Process ◽  
Dynamic Systems ◽  
Real Life ◽  
Temporal Logics ◽  
Business Process Modelling ◽  
Process Discovery ◽  
Event Log ◽  
Computational Properties

Temporal logics over finite traces have recently seen wide application in a number of areas, from business process modelling, monitoring, and mining to planning and decision making. However, real-life dynamic systems contain a degree of uncertainty which cannot be handled with classical logics. We thus propose a new probabilistic temporal logic over finite traces using superposition semantics, where all possible evolutions are possible, until observed. We study the properties of the logic and provide automata-based mechanisms for deriving probabilistic inferences from its formulas. We then study a fragment of the logic with better computational properties. Notably, formulas in this fragment can be discovered from event log data using off-the-shelf existing declarative process discovery techniques.

A review of temporal logics

1989 ◽  
Vol 4 (2) ◽  
pp. 141-162 ◽  
Author(s):  
Derek Long
Keyword(s):  
Artificial Intelligence ◽  
Temporal Logic ◽  
Temporal Reasoning ◽  
Order Logic ◽  
First Order Logic ◽  
Temporal Logics ◽  
Detailed Review ◽  
First Order ◽  
Reasoning Tasks

AbstractA series of temporal reasoning tasks are identified which motivate the consideration and application of temporal logics in artificial intelligence. There follows a discussion of the broad issues involved in modelling time and constructing a temporal logic. The paper then presents a detailed review of the major approaches to temporal logics: first-order logic approaches, modal temporal logics and reified temporal logics. The review considers the most significant exemplars within the various approaches, including logics due to Russell, Hayes and McCarthy, Prior, McDermott, Allen, Kowalski and Sergot. The logics are compared and contrasted, particularly in their treatments of change and action, the roles they seek to fulfil and the underlying models of time on which they rest. The paper concludes with a brief consideration of the problem of granularity—a problem of considerable significance in temporal reasoning, which has yet to be satisfactorily treated in a temporal logic.

scholarly journals Special Issue: Temporal Logic in Engineering

1999 ◽  
Vol 13 (2) ◽  
pp. 65-65
Author(s):  
EPHRAIM NISSAN
Keyword(s):  
Artificial Intelligence ◽  
Petri Nets ◽  
Temporal Logic ◽  
Special Issue ◽  
Temporal Logics ◽  
Modal Operators ◽  
Standard Part ◽  
Temporal Models

Logic-based models are thriving within artificial intelligence. A great number of new logics have been defined, and their theory investigated. Epistemic logics introduce modal operators for knowledge or belief; deontic logics are about norms, and introduce operators of deontic necessity and possibility (i.e., obligation or prohibition). And then we have a much investigated class—temporal logics—to whose application to engineering this special issue is devoted. This kind of formalism deserves increased widespread recognition and application in engineering, a domain where other kinds of temporal models (e.g., Petri nets) are by now a fairly standard part of the modelling toolbox.

scholarly journals Bunched Hypersequent Calculi for Distributive Substructural Logics

10.29007/ngp3 ◽  
2018 ◽  
Author(s):  
Agata Ciabattoni ◽  
Revantha Ramanayake
Keyword(s):  
Large Class ◽  
General Rule ◽  
Expressive Power ◽  
Substructural Logics ◽  
Cut Elimination ◽  
Lambek Calculus ◽  
Hypersequent Calculi

We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.

scholarly journals Ruina/basural: Lógicas temporales y espaciales de la ciudad de La Paz en Saenz y Viscarra

2021 ◽  
Vol 26 ◽  
pp. 158-180
Author(s):  
Irina Alexandra Feldman
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Space Time ◽  
Victor Hugo ◽  
National Narrative ◽  
Temporal Logics ◽  
La Paz ◽  
Queer Space ◽  
Spatio Temporal ◽  
The City

This article analyzes spatio-temporal logics in the representation of the city of La Paz in Imágenes Paceñas by Jaime Saenz and the urban chronicles of Víctor Hugo Viscarra. Juxtaposing the concepts of chrononormativity and queer time, it explores how linear temporal logic remains insufficient for the understanding of the city and its inhabitants in the two narrative projects. The article postulates that the marginal spaces of architectural ruins and garbage dumps, and the marginalized people who inhabit queer space-time are key to “revealing the hidden city” and understanding its contradictory place in the national narrative and space.

scholarly journals Two Temporal Logics of Contingency

2017 ◽  
Vol 12 (2) ◽  
pp. 121
Author(s):  
Matteo Pascucci
Keyword(s):  
Temporal Logic ◽  
Current Work ◽  
Temporal Logics ◽  
General Frames ◽  
Primitive Notion

This work concerns the use of operators for past and future con-tingency in Priorean temporal logic. We will develop a system namedCt, whose language includes a propositional constant and prove that(i) Ct is complete with respect to a certain class of general frames and(ii) the usual operators for past and future necessity are denable insuch system. Furthermore, we will introduce the extension Ctlin thatcan be interpreted on linear and transitive general frames. The theo-retical result of the current work is that contingency can be treatedas a primitive notion in reasoning about temporal modalities.

Sign in / Sign up

Export Citation Format

Share Document