Search

Mortensen studies dual intuitionistic logic by dualizing topos internal logic, but he did not study a sequent calculus. In this paper I present a sequent calculus for complement-topos logic, which throws some light on the problem of giving a dualization for LJ.

The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective. However, what if we go a step further and ask about the meaning of a proof as a whole? In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs. Two questions are central here. First of all, if we have two (syntactically) different derivations, does this always lead to a difference, firstly, in sense, and secondly, in denotation? The other question is about the relation between different kinds of proof systems (here: natural deduction vs. sequent calculi) with respect to this distinction. Do the different forms of representing a proof necessarily correspond to a difference in how the inferential steps are given? In our framework it will be possible to identify denotation as well as sense of proofs not only within one proof system but also between different kinds of proof systems. Thus, we give an account to distinguish a mere syntactic divergence from a divergence in meaning and a divergence in meaning from a divergence of proof objects analogous to Frege's distinction for singular terms and sentences., Comment: Post-peer-review, pre-copyedit version of article, published version available open access under DOI: 10.1007/s10992-020-09577-2

In this paper we discuss sequent calculi for the propositional fragment of the logic of HYPE. The logic of HYPE was recently suggested by Leitgeb (Journal of Philosophical Logic 48:305–405, 2019) as a logic for hyperintensional contexts. On the one hand we introduce a simple $$\mathbf{G1}$$ G 1 -system employing rules of contraposition. On the other hand we present a $$\mathbf{G3}$$ G 3 -system with an admissible rule of contraposition. Both systems are equivalent as well as sound and complete proof-system of HYPE. In order to provide a cut-elimination procedure, we expand the calculus by connections as introduced in Kashima and Shimura (Mathematical Logic Quarterly 40:153–172, 1994).

In this study, new sequent calculi for a minimal quantum logic (\(\bf MQL\)) are discussed that involve an implication. The sequent calculus \(\bf GO\) for \(\bf MQL\) was established by Nishimura, and it is complete with respect to ortho-models (O-models). As \(\bf GO\) does not contain implications, this study adopts the strict implication and constructs two new sequent calculi \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) as the expansions of \(\bf GO\). Both \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) are complete with respect to the O-models. In this study, the completeness and decidability theorems for these new systems are proven. Furthermore, some details pertaining to new rules and the strict implication are discussed.

In the natural deduction system for classical propositional logic given by G. Gentzen, there are some inference rules with assumptions discharged by the rule. D. Prawitz calls such inference rules improper, and others proper. Improper inference rules are more complicated and are often harder to understand than the proper ones. In the present paper, we distinguish between proper and improper derivations by using sequent systems. Specifically, we introduce a sequent system \(\vdash_{\bf Sc}\) for classical propositional logic with only structural rules, and prove that \(\vdash_{\bf Sc}\) does not allow improper derivations in general. For instance, the sequent \(\Rightarrow p \to q\) cannot be derived from the sequent \(p \Rightarrow q\) in \(\vdash_{\bf Sc}\). In order to prove the failure of improper derivations, we modify the usual notion of truth valuation, and using the modified valuation, we prove the completeness of \(\vdash_{\bf Sc}\). We also consider whether an improper derivation can be described generally by using \(\vdash_{\bf Sc}\).

In recent years, some theorists have argued that the clogics are not only defined by their inferences, but also by their metainferences. In this sense, logics that coincide in their inferences, but not in their metainferences were considered to be different. In this vein, some metainferential logics have been developed, as logics with metainferences of any level, built as hierarchies over known logics, such as $$\mathbf {ST}, \mathbf {LP}, \mathbf {K_3}$$ , and $$\mathbf {TS}$$ . What is distinctive of these metainferential logics is that they are mixed, i.e. the standard for the premises and the conclusion is not necessarily the same. However, so far, all of these systems have been presented following a semantical standpoint, in terms of valuations based on the Strong Kleene truth-tables. In this article, we provide sound and complete sequent-calculi for the valid inferences and the invalid inferences of the logics $$\mathbf {ST}, \mathbf {LP}, \mathbf {K_3}$$ and $$\mathbf {TS}$$ , and introduce an algorithm that allows obtaining sound and complete sequent-calculi for the global validities and the global invalidities of any metainferential logic of any level.

To investigate the relationship between logical reasoning and majority voting, we introduce logic with groups Lg in the style of Gentzen’s sequent calculus, where every sequent is indexed by a group of individuals. We also introduce the set-theoretical semantics of Lg, where every formula is interpreted as a certain closed set of groups whose members accept that formula. We present the cut-elimination theorem, and the soundness and semantic completeness theorems of Lg. Then, introducing an inference rule representing majority voting to Lg, we introduce logic with majority voting Lv. Formalizing the discursive paradox in judgment aggregation theory, we show that Lv is inconsistent. Based on the premise-based and conclusion-based approaches to avoid the paradox, we introduce logic with majority voting for axioms Lva, where majority voting is applied only to non-logical axioms as premises to construct a proof in Lg, and logic with majority voting for conclusions Lvc, where majority voting is applied only to the conclusion of a proof in Lg. We show that both Lva and Lvc are syntactically complete and consistent, and we construct collective judgments based on the provability in Lva and Lvc, respectively. Then, we discuss how these systems avoid the discursive paradox.

Based on the framework of disjunctive propositional logic, we first provide a syntactic representation for Scott domains. Precisely, we establish a category of consistent disjunctive sequent calculi with consequence relations, and show it is equivalent to that of Scott domains with Scott-continuous functions. Furthermore, we illustrate the approach to solving recursive domain equations by introducing some standard domain constructions, such as lifting and sums. The subsystems relation on consistent finitary disjunctive sequent calculi makes these domain constructions continuous. Solutions to recursive domain equations are given by constructing the least fixed point of a continuous function.

In this study, falsification-aware semantics and sequent calculi for first-order classical logic are introduced and investigated. These semantics and sequent calculi are constructed based on a falsification-aware setting for first-order Nelson constructive three-valued logic (N3). In fact, these semantics and sequent calculi are regarded as those for a classical variant of N3 (i.e., a classical variant of N3 is identical to first-order classical logic). The completeness and cut-elimination theorems for the proposed semantics and sequent calculi are proved using Schutte’s method. Similar results for the propositional case are also obtained.

A sequent calculus with the subformula property has long been recognised as a highly favourable starting point for the proof theoretic investigation of a logic. However, most logics of interest cannot be presented using a sequent calculus with the subformula property. In response, many formalisms more intricate than the sequent calculus have been formulated. In this work we identify an alternative: retain the sequent calculus but generalise the subformula property to permit specific axiom substitutions and their subformulas. Our investigation leads to a classification of generalised subformula properties and is applied to infinitely many substructural, intermediate, and modal logics (specifically: those with a cut-free hypersequent calculus). We also develop a complementary perspective on the generalised subformula properties in terms of logical embeddings. This yields new complexity upper bounds for contractive-mingle substructural logics and situates isolated results on the so-called simple substitution property within a general theory.

We examine the set of formula-to-formula valid inferences of Classical Logic, where the premise and the conclusion share at least a propositional variable in common. We review the fact, already proved in the literature, that such a system is identical to the first-degree entailment fragment of R. Epstein's Relatedness Logic, and that it is a non-transitive logic of the sort investigated by S. Frankowski and others. Furthermore, we provide a semantics and a calculus for this logic. The semantics is defined in terms of a \(p\)-matrix built on top of a 5-valued extension of the 3-element weak Kleene algebra, whereas the calculus is defined in terms of a Gentzen-style sequent system where the left and right negation rules are subject to linguistic constraints.

In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding BD+ into BDi and the McKinsey–Tarski theorem for embedding BDi into BDm.

Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.

In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti (1936) and Reichenbach (1935, 1944) on the one hand, and by Cooper (Inquiry, 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic, 49, 245–260, 2008) on the other. Here we provide the proof theory for the resulting logics and , using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: allows for algebraic completeness, but not for the construction of a canonical model, while fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects.

The paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is proved in a constructive way for sequent calculi adequate for all logics under consideration.

Lattice logic, bilattice logic, and paraconsistent quantum logic are investigated based on monosequent systems. Paraconsistent quantum logic is an extension of lattice logic, and bilattice logic is an extension of paraconsistent quantum logic. Monosequent system is a sequent calculus based on the restricted sequent that contains exactly one formula in both the antecedent and succedent. It is known that a completeness theorem with respect to a lattice-valued semantics holds for a monosequent system for lattice logic. A completeness theorem with respect to a lattice-valued semantics is proved for paraconsistent quantum logic, and a completeness theorem with respect to a bilattice-valued semantics is proved for bilattice logic. Some syntactical properties, including cut-elimination and duality, are also investigated for the monosequent systems for these logics.

In this paper we consider the optimal dividend problem for an insurance company whose surplus follows a classical Cramer-Lundberg process with a feature of self-exciting. A Hawkes process is applied so that the occurrence of a jump in the claims triggers more sequent jumps. We show that the optimal value function is a unique viscosity solution of the associated Hamilton-Jacobi-Bellman equation with a given boundary condition and declare its concavity. We introduce a barrier curve strategy and verify its optimality. Finally, some numerical results are exhibited.

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak Kőnig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

We continue the investigation of the first paper where we studied logics with various negations including empirical negation and co-negation. We established how such logics can be treated uniformly with R. Sylvan's CCω as the basis. In this paper we use this result to obtain cut-free labelled sequent calculi for the logics.

The language of Belnap–Dunn modal logic $${\mathscr {L}}_0$$ expands the language of Belnap–Dunn four-valued logic (having constant symbols for the values 0 and 1) with the modal operator $$\Box $$ . We introduce the polarity semantics for $${\mathscr {L}}_0$$ and its two expansions $${\mathscr {L}}_1$$ and $${\mathscr {L}}_2$$ with value operators. The local finitary consequence relation $$\models _4^k$$ in the language $${\mathscr {L}}_k$$ with respect to the class of all frames is axiomatized by a sequent system $$\mathsf {S}_k$$ where $$k=0, 1, 2$$ . We prove by using translations between sequents and formulas that these languages under the polarity semantics have the same expressive power on the level of frames with the language $${\mathscr {L}}_0$$ under the relational semantics for classical modal logic.

In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen's classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ., Paper presented at the 36th International Conference on Logic Programming (ICLP 2019), University Of Calabria, Rende (CS), Italy, September 2020, 16 pages

Paraconsistent logics constitute an important class of formalisms dealing with non-trivial reasoning from inconsistent premisses. In this paper, we introduce uniform axiomatisations for a family of nonmonotonic paraconsistent logics based on minimal inconsistency in terms of sequent-type proof systems. The latter are prominent and widely-used forms of calculi well-suited for analysing proof search. In particular, we provide sequent-type calculi for Priest's three-valued minimally inconsistent logic of paradox, and for four-valued paraconsistent inference relations due to Arieli and Avron. Our calculi follow the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti and Olivetti, whose distinguishing feature is the use of a so-called rejection calculus for axiomatising invalid formulas. In fact, we present a general method to obtain sequent systems for any many-valued logic based on minimal inconsistency, yielding the calculi for the logics of Priest and of Arieli and Avron as special instances., In Proceedings ICLP 2020, arXiv:2009.09158

C. I. Lewis’ systems were the first axiomatisations of modal logics. However some of those systems are non-normal modal logics, since they do not admit a full rule of necessitation, but only a restricted version thereof. We provide G3-style labelled sequent calculi for Lewis’ non-normal propositional systems. The calculi enjoy good structural properties, namely admissibility of structural rules and admissibility of cut. Furthermore they allow for straightforward proofs of admissibility of the restricted versions of the necessitation rule. We establish completeness of the calculi and we discuss also related systems.

One of the most fundamental properties of a proof system is analyticity, expressing the fact that a proof of a given formula F only uses subformulas of F. In sequent calculus, this property is usually proved by showing that the cut rule is admissible, i.e., the introduction of the auxiliary lemma A in the reasoning “if A follows from B and C follows from A, then C follows from B” can be eliminated. Mathematically, this means that we can inline the intermediate step A to have a direct proof of C from the hypothesis B. More importantly, the proof of cut-elimination shows that the proof of C follows directly from the axiomatic theory and B (and no external lemmas are needed). The proof of cut-elimination is usually a tedious process through several proof transformations, thus requiring the assistance of (semi-)automatic procedures to avoid mistakes. In a previous work by Miller and Pimentel, linear logic ( LL ) was used as a logical framework for establishing sufficient conditions for cut-elimination of object logics (OL). The OL's inference rules were encoded as an LL theory and an easy-to-verify criterion sufficed to establish the cut-elimination theorem for the OL at hand. Using such procedure, analyticity of logical systems such as LK (classical logic), LJ (intuitionistic logic) and substructural logics such as MALL (multiplicative additive LL ) was proved within the framework. However, there are many logical systems that cannot be adequately encoded in LL , the most symptomatic cases being sequent systems for modal logics. In this paper we use a linear-nested sequent ( LNS ) presentation of SLL (a variant of linear logic with subexponentials) and show that it is possible to establish a cut-elimination criterion for a larger class of logical systems, including LNS proof systems for K , 4 , KT , KD , S4 and the multi-conclusion LNS system for intuitionistic logic ( mLJ ). Impressively enough, the sufficient conditions for cut-elimination presented here remain as simple as the one proposed by Miller and Pimentel. The key ingredient in our developments is the use of the right formalism: we adopt LNS based OL systems, instead of sequent ones. This not only provides a neat encoding procedure of OLs into SLL , but it also allows for the use of the meta-theory of SLL to establish fundamental meta-properties of the encoded OLs. We thus contribute with procedures for checking cut-elimination of several logical systems that are widely used in philosophy, mathematics and computer science.

We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi. Problems in programming 2020; 2-3: 182-197

Free logics is a family of first-order logics which came about as a result of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that (i) the domain of interpretation is not empty, (ii) every name denotes exactly one object in the domain and (iii) the quantifiers have existential import. Free logics usually reject the claim that names need to denote in (ii), and of the systems considered in this paper, the positive free logic concedes that some atomic formulas containing non-denoting names (namely self-identity) are true, while negative free logic rejects even the latter claim. Inclusive logics, which reject (i), are likewise considered. These logics have complex and varied axiomatizations and semantics, and the goal of this paper is to present an orderly examination of the various systems and their mutual relations. This is done by first offering a formalization, using sequent calculi which possess all the desired structural properties of a good proof system, including admissibility of contraction and cut, while streamlining free logics in a way no other approach has. We then present a simple and unified system of abstract semantics, which allows for a straightforward demonstration of the meta-theoretical properties, and offers insights into the relationship between different logics (free and classical). The final part of this paper is dedicated to extending the system with modalities by using a labeled sequent calculus, and here we are again able to map out the different approaches and their mutual relations using the same framework.

We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).

We show that the replacement rule of the sequent calculi ${\bf G3[mic]}^= $ in [8] can be replaced by the simpler rule in which one of the principal formulae is not repeated in the premiss.

Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot's free deduction. The elimination rules are "general," but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms for natural deduction proofs as in the Curry-Howard isomorphism. Addition of an indirect proof rule yields classical single-conclusion versions of these systems. Gentzen's standard systems arise as special cases., Comment: 42 pp

Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for N4C and N4C+ are proved.

We define and investigate Frege systems for quantified Boolean formulas (QBF). For these new proof systems, we develop a lower bound technique that directly lifts circuit lower bounds for a circuit class C to the QBF Frege system operating with lines from C. Such a direct transfer from circuit to proof complexity lower bounds has often been postulated for propositional systems but had not been formally established in such generality for any proof systems prior to this work. This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponential lower bound for QBF Frege systems operating with AC0[p] circuits. In contrast, any non-trivial lower bound for propositional AC0[p]-Frege constitutes a major open problem. Improving these lower bounds to unrestricted QBF Frege tightly corresponds to the major problems in circuit complexity and propositional proof complexity. In particular, proving a lower bound for QBF Frege systems operating with arbitrary P/poly circuits is equivalent to either showing a lower bound for P/poly or for propositional extended Frege (which operates with P/poly circuits). We also compare our new QBF Frege systems to standard sequent calculi for QBF and establish a correspondence to intuitionistic bounded arithmetic. This research was supported by grant nos. 48138 and 60842 from the John Templeton Foundation, EPSRC grant EP/L024233/1, and a Doctoral Prize Fellowship from EPSRC (third author). The second author was funded by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007–2013)/ERC grant agreement no. 279611 and under the European Union’s Horizon 2020 Research and Innovation Programme/ERC grant agreement no. 648276 AUTAR. The fourth author was supported by the Austrian Science Fund (FWF) under project number P28699 and by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2014)/ERC Grant Agreement no. 61507. Part of this work was done when Beyersdorff and Pich were at the University of Leeds and Bonacina at Sapienza University Rome.

Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics ECTL and ECT L + were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic CT L ⋆ , often considered as ‘the full branching-time logic’ overcomes these restrictions on expressing fairness. However, CT L ⋆ is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for CT L ⋆ , while one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more ‘natural’ being more friendly for human understanding. These two considerations lead to the following problem - are there logics that have richer expressiveness than ECT L + , allowing the formulation of a new range of fairness constraints with ‘until’ operator, yet ‘simpler’ than CT L ⋆ , and for which a one-pass tableau can be developed? Here we give a positive answer to this question, introducing a sub-logic of CT L ⋆ called ECT L # , its tree-style one-pass tableau, and an algorithm for obtaining a systematic tableau, for any given admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi. Our results also open a prospect of relevant developments of the automation and implementation of the tableau method for ECT L # , and of a dual sequent calculi.

Inspired by the efficient proof procedures discussed in {\em Computability logic} \cite{Jap03,Japic,Japfin}, we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system and has the following features: (a)~ it views sequents as games between the machine and the environment, and (b)~ it views proofs as a winning strategy of the machine. From this game-based viewpoint, a poweful heuristic can be extracted and a fair degree of determinism in proof search can be obtained. This article proposes a new deductive system LKg with respect to first-order logic and proves its soundness and completeness. We also discuss LKg', a variant of LKg with some optimizations added., Comment: 6 pages. Some optimizations are added

Various types of calculi (Hilbert, Gentzen sequent, resolution calculi, tableaux) for propositional linear temporal logic (PLTL) have been invented. In this paper, a sound and complete loop-type sequent calculus $$\mathbf{G} _\text {L}{} \mathbf{T} $$ for PLTL with the temporal operators “next” and “henceforth always” ( $${\mathbf{PLTL}}^{n,a}$$ ) is considered at first. We prove that all rules of $$\mathbf{G} _\text {L}{} \mathbf{T} $$ are invertible and that the structural rules of weakening and contraction, as well as the rule of cut, are admissible in $$\mathbf{G} _\text {L}{} \mathbf{T} $$ . We describe a decision procedure for $${\mathbf{PLTL}}^{n,a}$$ based on the introduced calculus $$\mathbf{G} _\text {L}{} \mathbf{T} $$ . Afterwards, we introduce a sound and complete sequent calculus $$\mathbf{G} _\text {L}{} \mathbf{T} ^\mathcal {U}$$ for PLTL with the temporal operators “next” and “until”.

We propose a new least squares finite element method to solve the Poisson equation. By using a piecewisely irrotational space to approximate the flux, we split the classical method into two sequential steps. The first step gives the approximation of flux in the new approximation space and the second step can use flexible approaches to give the pressure. The new approximation space for flux is constructed by patch reconstruction with one unknown per element consisting of piecewisely irrotational polynomials. The error estimates in the energy norm and $L^2$ norm are derived for the flux and the pressure. Numerical results verify the convergence order in error estimates, and demonstrate the flexibility and particularly the great efficiency of our method.

The physical features of ultra-wideband signals are considered. The well-known technical solutions for synchronizing signals during their accumulation are analyzed. The necessity of randomizing the temporal parameters of the following pulse their accumulation is substantiated. The main steps of the technique are described that allow the simultaneous solution of the problem of detecting sequential signals by accumulating them on the receiving side and synchronizing them. An assessment of the computational complexity of the technique is presented and recommendations for its practical application are given.

The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. Interestingly enough, we show that for any system equipped with a reasonable exponential modality the following holds: if the system enjoys cut elimination and substitution to the full extent, then the system necessarily violates Lambek’s restriction. Nevertheless, we show that two of the three conditions can be implemented. Namely, we design a system with Lambek’s restriction and cut elimination and another system with Lambek’s restriction and substitution. For both calculi, we prove that they are undecidable, even if we take only one of the two divisions provided by the Lambek calculus. The system with cut elimination and substitution and without Lambek’s restriction is folklore and known to be undecidable.

It is proved in this paper that the number of minimal tautologies for any given logic tautology of size п can be an exponential function in п, and it is also proved that for every tautology of the given logic there is some minimal tautology such that the number of its sequential form proof steps is equal to minimal steps in the proof of sequential form for the given tautology in cut-free sequent systems for classical, intuitionistic, Joganssons and monotone logics.

The minimal weakening $${{\textsf {N}}}_0$$ of Belnap-Dunn logic under the polarity semantics for negation as a modal operator is formulated as a sequent system which is characterized by the class of all birelational frames. Some extensions of $${{\textsf {N}}}_0$$ with additional sequents as axioms are introduced. In particular, all three modal negation logics characterized by a frame with a single state are formalized as extensions of $${{\textsf {N}}}_0$$ . These logics have the finite model property and they are decidable.

We build a logical system named a conjunctive sequent calculus which is a conjunctive fragment of the classical propositional sequent calculus in the sense of proof theory. We prove that a special class of formulae of a consistent conjunctive sequent calculus forms a bounded complete continuous domain without greatest element (for short, a proper BC domain), and each proper BC domain can be obtained in this way. More generally, we present conjunctive consequence relations as morphisms between consistent conjunctive sequent calculi and build a category which is equivalent to that of proper BC domains with Scott-continuous functions. A logical characterization of purely syntactic form for proper BC domains is obtained.

This paper summarizes our efforts to aid human reasoning when verification fails through the use of two distinct Formalization Integrated Development Environments (F-IDEs) that we have developed. Both environments are modular and facilitate reasoning about the full behavior of object-based code. The first environment, referred to as the web-IDE, has been used for several years to teach aspects of formal specification and verification, including why and where verification conditions (VCs) arise and how to use them when verification fails. The second F-IDE, RESOLVE Studio, remains experimental, but is a more fully-fledged environment backed by a sequent-based VC generator that produces VCs with fewer extraneous givens. While the environments and VC generation techniques are necessarily language specific, the principles of alternative VC generation methods, F-IDE features, and observations about their impact on novices and experienced users are more generally applicable., In Proceedings AppFM 2021, arXiv:2111.07538