Proof-theoretical investigation of temporal logic with time gaps

In the paper, the first-order intuitionistic temporal logic sequent calculus LBJ is considered. The invertibility of some of the LBJ rules, syntactic admissibility of the structural rules and the cut rule in LBJ, as well as Harrop and Craig's interpolation theorems for LBJ are proved. Gentzen's midsequent theorem is proved for the LBJ' calculus which is obtained from LBJ by removing the antecedent disjunction rule from it. Published in Lietuvos Matematikos Rinkinys, Vol. 40, No. 3, pp. 255–276, July–September, 2000.     

Infinitary Calculus without Loop Rules for Restricted Sequents of the First-Order Linear Temporal Logic

A restricted first-order linear temporal logic with temporal operators next and always is considered. We prove that for this logic one can construct a sequential calculus without loop rules, i.e., the rules containing a duplication of the main formula in the premises of these rules. This paper continues the previous work of the author, where an infinitary calculus without loop rules on the logical level, but containing the traditional loop antecedent rule for the operator always, was constructed. In this paper, in order to remove this loop rule we introduce a nonlocal rule allowing us to eliminate loops in the process of the proof search. The soundness and >-completeness of the constructed calculus is proved.     

Glivenko Classes of Sequents for Temporal Logic with Time Gaps

Let LB be a sequent calculus of the first-order classical temporal logic TB with time gaps. Let, further, LBJ be the intuitionistic counterpart of LB. In this paper, we consider conditions under which a sequent is derivable in the calculus LBJ if and only if it is derivable in the calculus LB. Such conditions are defined for sequents with one formula in the succedent (purely Glivenko -classes) and for sequents with the empty succedent (Glivenko -classes).     

A chain rule for ?-subdifferentials with applications to approximate solutions in convex Pareto problems

In this work we obtain a chain rule for the approximate subdifferential considering a vector-valued proper convex function and its post-composition with a proper convex function of several variables nondecreasing in the sense of the Pareto order. We derive an interesting formula for the conjugate of a composition in the same framework and we prove the chain rule using this formula. To get the results, we require qualification conditions since, in the composition, the initial function is extended vector-valued. This chain rule extends analogous well-known calculus rules obtained when the functions involved are finite and it gives a complementary simple expression for other chain rules proved without assuming any qualification condition. As application we deduce the well-known calculus rule for the addition and we extend the formula for the maximum of functions. Finally, we use them and a scalarization process to obtain Kuhn-Tucker type necessary and sufficient conditions for approximate solutions in convex Pareto problems. These conditions extend other obtained in scalar optimization problems.     

Local computation in linear logic

This work deals with the exponential fragment of Girard's linear logic ([3]) without the contraction rule, a logical system which has a natural relation with the direct logic ([10], [7]). A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism ([6]) with respect to the logical system in question. MSC: 03B40, 03F05.     

The Penalty Functions Method and Multiplier Rules Based on the Mordukhovich Subdifferential

We show that the finite-dimensional Fritz John multiplier rule, which is based on the limiting/Mordukhovich subdifferential, can be proved by using differentiable penalty functions and the basic calculus tools in variational analysis. The corresponding Kuhn–Tucker multiplier rule is derived from the Fritz John multiplier rule by imposing a constraint qualification condition or the exactness of an ?₁ penalty function. Complementing the existing proofs, our proofs provide another viewpoint on the fundamental multiplier rules employing the Mordukhovich subdifferential.     

Conditioning of linear-quadratic two-stage stochastic optimization problems

In this paper a condition number for linear-quadratic two-stage stochastic optimization problems is introduced as the Lipschitz modulus of the multifunction assigning to a (discrete) probability distribution the solution set of the problem. Being the outer norm of the Mordukhovich coderivative of this multifunction, the condition number can be estimated from above explicitly in terms of the problem data by applying appropriate calculus rules. Here, a chain rule for the extended partial second-order subdifferential recently proved by Mordukhovich and Rockafellar plays a crucial role. The obtained results are illustrated for the example of two-stage stochastic optimization problems with simple recourse.     

Analysis of interpretability-accuracy tradeoff of fuzzy systems by multiobjective fuzzy genetics-based machine learning

This paper examines the interpretability-accuracy tradeoff in fuzzy rule-based classifiers using a multiobjective fuzzy genetics-based machine learning (GBML) algorithm. Our GBML algorithm is a hybrid version of Michigan and Pittsburgh approaches, which is implemented in the framework of evolutionary multiobjective optimization (EMO). Each fuzzy rule is represented by its antecedent fuzzy sets as an integer string of fixed length. Each fuzzy rule-based classifier, which is a set of fuzzy rules, is represented as a concatenated integer string of variable length. Our GBML algorithm simultaneously maximizes the accuracy of rule sets and minimizes their complexity. The accuracy is measured by the number of correctly classified training patterns while the complexity is measured by the number of fuzzy rules and/or the total number of antecedent conditions of fuzzy rules. We examine the interpretability-accuracy tradeoff for training patterns through computational experiments on some benchmark data sets. A clear tradeoff structure is visualized for each data set. We also examine the interpretability-accuracy tradeoff for test patterns. Due to the overfitting to training patterns, a clear tradeoff structure is not always obtained in computational experiments for test patterns.     

Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas

An infinitary calculus for a restricted fragment of the first-order linear temporal logic is considered. We prove that for this fragment one can construct the infinitary calculusG _Lω ^* without contraction on predicate formulas. The calculusG _Lω ^* possesses the following properties: (1) the succedent rule for the existential quantifier is included into the corresponding axiom; (2) the premise of the antecedent rule for the universal quantifier does not contain a duplicate of the main formula. The soundness and completness ofG _Lω ^* are also proved. Institute of Mathematics and Informatics, Akademijos 4, 2600 Vilnius, Lithuania. Translated from Lietuvos Matematikos Rinkinys, Vol. 39, No. 3, pp. 378–397, July–September, 1999. Translated by R. Lapinskas     

Multivector differential calculus

Universal geometric calculus simplifies and unifies the structure and notation of mathematics for all of science and engineering, and for technological applications. This paper treats the fundamentals of the multivector differential calculus part of geometric calculus. The multivector differential is introduced, followed by the multivector derivative and the adjoint of multivector functions. The basic rules of multivector differentiation are derived explicitly, as well as a variety of basic multivector derivatives. Finally factorization, which relates functions of vector variables and multivector variables is discussed, and the concepts of both simplicial variables and derivatives are explained. Everything is proven explicitly in a very elementary level step by step approach. The paper is thus intended to serve as reference material, providing a number of details, which are usually skipped in more advanced discussions of the subject matter. The arrangement of the material closely followschapter 2 of [3].     

On Commutative and Nonassociative Syntactic Calculi and Categorial Grammars

Two axiomatizations of the nonassociative and commutative Lambek syntactic calculus are given and their equivalence is proved. The first axiomatization employs Permutation as the only structural rule, the second one, with no Permutation rule, employs only unidirectional types. It is also shown that in the case of the Ajdukiewicz calculus an analogous equivalence is valid only in the case of a restricted set of formulas. Unidirectional axiomatizations are employed in order to establish the generative power of categorial grammars based on the nonassociative and commutative Lambek calculus with product. Those grammars produce CF-languages of finite degree generated by CF-grammars closed with respect to permutations.     

CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT

The aim of this paper is to extend the semantic analysis of tense logic in Rescher/Urquhart [3] to propositional dynamic logic without*. For this we develop a nested sequential calculus whose axioms and rules directly reflect the steps in the semantic analysis. It is shown that this calculus, with the cut rule omitted, is complete with respect to the standard semantics. It follows that cut elimination does hold for this nested sequential calculus. MSC: 03B45.     

The fuzzy intersection rule in variational analysis with applications

The fuzzy intersection rule for Fréchet normal cones in Asplund spaces was established by Mordukhovich and the author using the extremal principle, which appears more convenient to apply in some applications. In this paper, we present a complete discussion of this rule in various aspects. We show that the fuzzy intersection rule is another characterization of the Asplund property of the space. Various applications are considered as well. In particular, a complete set of fuzzy calculus rules for general lower semicontinuous functions are established.     

Mutation calculi

A (I)-mutation is a transition by one of the rules (p and q are variables; G₂ and G₂ are fixed words in A, containing no fewer than two letters;. A (II)-mutation (or polyploidy) is a transition by the rule p/pp. Rules (I)–(II) formalize the simplest mutations of the biological code. It is easy to construct analogous rules for many other types of mutations. Biological evolution can be represented as an evolution of words of genotypes; new genotypes are generated by applying the rules mentioned; an evolution tree is a tree of deductions in some mutation calculus (m.c.); the evolution process is the process of generation of deductions in a suitable probabilistic canonic m.c. Under natural assumptions some qualitative results (the inevitable extinction of any genotype, an estimate of the acceleration due to bisexual evolution, etc.) are established. Various constraints on the m.c. are studied (with the aim of modelling the typical features of evolution by minimal means). Very simple deductive means are sufficient for the representation of any enumerable set. For example, those m.c. are sufficient that contain only: 1) rules (Ia) and (Ic); 2) rule (II) and rule (Ia). It is proved that further constraints lead to decidable m.c.Results announced on Sept. 5 and 12, 1974.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 49, pp. 7–30, 1975.     

Distributive-Lattice Semantics of Sequent Calculi with Structural Rules

The goal of the paper is to develop a universal semantic approach to derivable rules of propositional multiple-conclusion sequent calculi with structural rules, which explicitly involve not only atomic formulas, treated as metavariables for formulas, but also formula set variables (viz., metavariables for finite sets of formulas), upon the basis of the conception of model introduced in (Fuzzy Sets Syst 121(3):27–37, 2001). One of the main results of the paper is that any regular sequent calculus with structural rules has such class of sequent models (called its semantics) that a rule is derivable in the calculus iff it is sound with respect to each model of the semantics. We then show how semantics of admissible rules of such calculi can be found with using a method of free models. Next, our universal approach is applied to sequent calculi for many-valued logics with equality determinant. Finally, we exemplify this application by studying sequent calculi for some of such logics.      

Labeled sequent calculus for justification logics

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for $\mathsf{S4LPN}$ based on Artemov–Fitting models.     

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). Received: February 15, 1996     

Asplund空间中方向上导数和序列法紧性质分析法则

研究了广义微分结构中的集合方向Mordukhovich法锥、集值映射的方向上导数,以及集合和集值映射的方向序列法紧性的分析法则. 基于集合方向Mordukhovich法锥的交集法则,在方向内半紧性假设下,建立了集合的方向Mordukhovich法锥、集值映射的方向上导数的分析法则.此外,借助Asplund乘积空间中集合的方向序列法紧性的交集法则, 在方向内半紧性和相应的规范条件下,建立了集合和集值映射的(部分)方向序列法紧性的加法、逆像、复合等法则.     

Circular proofs for the modal mu-calculus

Inspired by Stirling's tableau proofs [4] we introduce a finite, cut-free sound and complete sequent calculus for the modal mu-calculus. Proofs in this system are finite trees in which leaves are either axioms or assumptions that are discharged by a specific rule of the calculus. The discharge rules provide a way to unfold assumptions motivating the name circular proofs. (© 2016 Wiley-VCH Verlag GmbH & Co. KGaA, Weinheim)