LINEAR TIME IN HYPERSEQUENT FRAMEWORK

ANDRZEJ INDRZEJCZAK

doi:10.1017/bsl.2016.2

LINEAR TIME IN HYPERSEQUENT FRAMEWORK

Bulletin of Symbolic Logic ◽

10.1017/bsl.2016.2 ◽

2016 ◽

Vol 22 (1) ◽

pp. 121-144 ◽

Cited By ~ 7

Author(s):

ANDRZEJ INDRZEJCZAK

Keyword(s):

Proof Theory ◽

Linear Time ◽

Expressive Power ◽

Sequent Calculi ◽

Temporal Logics ◽

Structural Rules ◽

Proof Systems ◽

Nonclassical Logics ◽

Time Flow ◽

Basic Calculus

AbstractHypersequent calculus (HC), developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi (SC). In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite (multi)sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules (three for future-necessity and three dual rules for past-necessity). Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents.

Download Full-text

On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

Modeling and Analysis of Information Systems ◽

10.18255/1818-1015-2021-4-356-371 ◽

2021 ◽

Vol 28 (4) ◽

pp. 356-371

Author(s):

Anton Romanovich Gnatenko ◽

Vladimir Anatolyevich Zakharov

Keyword(s):

Model Checking ◽

Temporal Logic ◽

Linear Time ◽

Complete Solution ◽

Reactive Systems ◽

Expressive Power ◽

Regular Languages ◽

Specification Languages ◽

Temporal Logics ◽

Emptiness Problem

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

Download Full-text

A Tableau Proof System with Names for Modal Mu-calculus

10.29007/lwqm ◽

2018 ◽

Author(s):

Colin Stirling

Keyword(s):

Modal Logic ◽

Expressive Power ◽

Proof System ◽

Temporal Logics ◽

General Issue ◽

Proof Systems

Howard Barringer was a pioneer in the study of temporal logics withfixpoints. Their addition adds considerable expressive power.One general issue is how to defineproof systems for such logics. Here we examine proof systems formodal logic with fixpoints. We present a tableau proof systemfor checking validity of formulaswhich uses names to keep track of unfoldings of fixpoint variables.

Download Full-text

Generalized quantification as substructural logic

Journal of Symbolic Logic ◽

10.2307/2275797 ◽

1996 ◽

Vol 61 (3) ◽

pp. 1006-1044 ◽

Cited By ~ 2

Author(s):

Natasha Alechina ◽

Michiel Van Lambalgen

Keyword(s):

Proof Theory ◽

Sequent Calculus ◽

Substructural Logic ◽

Generalized Quantifiers ◽

Accessibility Relation ◽

Dependence Relation ◽

Structural Rules ◽

First Order ◽

Proof Systems ◽

Structured Objects

AbstractWe show how sequent calculi for some generalized quantifiers can be obtained by generalizing the Herbrand approach to ordinary first order proof theory. Typical of the Herbrand approach, as compared to plain sequent calculus, is increased control over relations of dependence between variables. In the case of generalized quantifiers, explicit attention to relations of dependence becomes indispensible for setting up proof systems. It is shown that this can be done by turning variables into structured objects, governed by various types of structural rules. These structured variables are interpreted semantically by means of a dependence relation. This relation is an analogue of the accessibility relation in modal logic. We then isolate a class of axioms for generalized quantifiers which correspond to first-order conditions on the dependence relation.

Download Full-text

Proof Theory of the Cut Rule

10.1093/oso/9780198748991.003.0010 ◽

2018 ◽

Author(s):

J. R. B. Cockett ◽

R. A. G. Seely

Keyword(s):

Proof Theory ◽

Graphical Representation ◽

Basic Component ◽

Graphical Representations ◽

Mathematical Language ◽

Basic Logic ◽

Cut Rule ◽

Structural Rules ◽

The One ◽

Categorical Semantics

This chapter describes the categorical proof theory of the cut rule, a very basic component of any sequent-style presentation of a logic, assuming a minimum of structural rules and connectives, in fact, starting with none. It is shown how logical features can be added to this basic logic in a modular fashion, at each stage showing the appropriate corresponding categorical semantics of the proof theory, starting with multicategories, and moving to linearly distributive categories and *-autonomous categories. A key tool is the use of graphical representations of proofs (“proof circuits”) to represent formal derivations in these logics. This is a powerful symbolism, which on the one hand is a formal mathematical language, but crucially, at the same time, has an intuitive graphical representation.

Download Full-text

The Method of Socratic Proofs Meets Correspondence Analysis

Bulletin of the Section of Logic ◽

10.18778/0138-0680.48.2.02 ◽

2019 ◽

Vol 48 (2) ◽

pp. 99-116

Author(s):

Dorota Leszczyńska-Jasion ◽

Yaroslav Petrukhin ◽

Vasilyi Shangin

Keyword(s):

Correspondence Analysis ◽

Boolean Functions ◽

Propositional Logic ◽

Sequent Calculus ◽

Sequent Calculi ◽

Classical Propositional Logic ◽

Logic Of Questions ◽

Proof Systems

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic (i.e. pertaining to the logic of questions) calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for the method of Socratic proofs. Correspondence analysis is Kooi and Tamminga's technique for designing proof systems. In this paper it is used to consider sequent calculi with non-branching (the only exception being the rule of cut), invertible rules for the negation fragment of classical propositional logic and its extensions by binary Boolean functions.

Download Full-text