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.      

Sequent calculi for branching time temporal logics of knowledge and beliefwith awareness: Completeness and decidability

In this paper, we consider branching time temporal logic CT L with epistemic modalities for knowledge (belief) and with awareness operators. These logics involve the discrete-time linear temporal logic operators “next” and “until” with the branching temporal logic operator “on all paths”. In addition, the temporal logic of knowledge (belief) contains an indexed set of unary modal operators “agent i knows” (“agent i believes”). In a language of these logics, there are awareness operators. For these logics, we present sequent calculi with a restricted cut rule. Thus, we get proof systems where proof-search becomes decidable. The soundness and completeness for these calculi are proved. Published in Lietuvos Matematikos Rinkinys, Vol. 47, No. 3, pp. 328–340, July–September, 2007.     

Truncated regularized Newton method for convex minimizations

Recently, Li et al. (Comput. Optim. Appl. 26:131–147, 2004) proposed a regularized Newton method for convex minimization problems. The method retains local quadratic convergence property without requirement of the singularity of the Hessian. In this paper, we develop a truncated regularized Newton method and show its global convergence. We also establish a local quadratic convergence theorem for the truncated method under the same conditions as those in Li et al. (Comput. Optim. Appl. 26:131–147, 2004). At last, we test the proposed method through numerical experiments and compare its performance with the regularized Newton method. The results show that the truncated method outperforms the regularized Newton method. The work was supported by the 973 project granted 2004CB719402 and the NSF project of China granted 10471036.     

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.     

Contraction-free sequent calculi for geometric theories with an application to Barr's theorem

 Geometric theories are presented as contraction- and cut-free systems of sequent calculi with mathematical rules following a prescribed rule-scheme that extends the scheme given in Negri and von Plato (1998). Examples include cut-free calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable. Received: 18 April 2001 / Published online: 10 October 2002 Mathematics Subject Classification (2000): 03F05, 18C10, 18B15 Key words or phrases: Cut elimination – Geometric theories – Barr's theorem     

Perturbation bounds for polynomials

Using two different elementary approaches we derive a global and a local perturbation theorem on polynomial zeros that significantly improve the results of Ostrowski (Acta Math 72:99–257, 1940), Elsner et al. (Linear Algebra Appl 142:195–209, 1990). A comparison of different perturbation bounds shows that our results are better in many cases than the similar local result of Beauzamy (Can Math Bull 42(1):3–12, 1999). Using the matrix theoretical approach we also improve the backward stability result of Edelman and Murakami (Proceedings of the Fifth SIAM Conference on Applied Linear Algebra, SIAM, Philapdelphia, 1994; Math Comput 64:210–763, 1995).     

An example of a commutative basic algebra which is not an MV-algebra

Many algebras arising in logic have a lattice structure with intervals being equipped with antitone involutions. It has been proved in [CHK1] that these lattices are in a one-to-one correspondence with so-called basic algebras. In the recent papers [BOTUR, M.—HALAŠ, R.: Finite commutative basic algebras are MV-algebras, J. Mult.-Valued Logic Soft Comput. (To appear)]. and [BOTUR, M.—HALAŠ, R.: Complete commutative basic algebras, Order 24 (2007), 89–105] we have proved that every finite commutative basic algebra is an MV-algebra, and that every complete commutative basic algebra is a subdirect product of chains. The paper solves in negative the open question posed in [BOTUR, M.—HALAŠ, R.: Complete commutative basic algebras, Order 24 (2007), 89–105] whether every commutative basic algebra on the interval [0, 1] of the reals has to be an MV-algebra.     

A note on the conditional probability of <Emphasis Type="Italic">IF</Emphasis>-events

We formulate a version of the conditional probability of an IF-event considering the Łukasiewicz operations with IF-sets. Also some properties of conditional probability are proved. The results are strengthenings of preceding ones published in [LENDELOVá, K.: Conditional IF-probability. In: Soft Methods for Integrated Uncertainty Modelling. Proceedings of the 2006 InternationalWorkshop on Soft Methods in Probability and Statistics (SMPS 2006), Bristol, UK, September 5–7, 2006. Adv. Soft Comput., Springer-Verlag, Berlin, 2006, pp. 275–283]. The paper was supported by Grant VEGA 1/0539/08.     

On the algebraic structure of linear, relevance, and fuzzy logics

 Substructural logics are obtained from the sequent calculi for classical or intuitionistic logic by suitably restricting or deleting some or all of the structural rules (Restall, 2000; Ono, 1998). Recently, this field of research has come to encompass a number of logics - e.g. many fuzzy or paraconsistent logics - which had been originally introduced out of different, possibly semantical, motivations. A finer proof-theoretical analysis of such logics, in fact, revealed that it was possible to subsume them under the previous definition (see e.g. Aguzzoli and Ciabattoni, 2000). Although proof systems for substructural logics are currently being investigated with remarkable success, their algebraic models do not seem equally satisfactory. In fact: (i) such structures are often very weak, i.e. they do not possess many interesting algebraic properties; (ii) as a consequence, their theories of ideals, congruences, and representation are as a rule scarcely developed, or even lacking. In this paper, we address these difficulties. Received: 18 February 2000 / Published online: 12 December 2001     

New sequent calculi for Visser's Formal Propositional Logic

Two cut‐free sequent calculi which are conservative extensions of Visser's Formal Propositional Logic (FPL) are introduced. These satisfy a kind of subformula property and by this property the interpolation theorem for FPL are proved. These are analogies to Aghaei‐Ardeshir's calculi for Visser's Basic Propositional Logic.     

Extending the applicability of the Gauss–Newton method under average Lipschitz–type conditions

We extend the applicability of the Gauss–Newton method for solving singular systems of equations under the notions of average Lipschitz–type conditions introduced recently in Li et al. (J Complex 26(3):268–295, 2010). Using our idea of recurrent functions, we provide a tighter local as well as semilocal convergence analysis for the Gauss–Newton method than in Li et al. (J Complex 26(3):268–295, 2010) who recently extended and improved earlier results (Hu et al. J Comput Appl Math 219:110–122, 2008; Li et al. Comput Math Appl 47:1057–1067, 2004; Wang Math Comput 68(255):169–186, 1999). We also note that our results are obtained under weaker or the same hypotheses as in Li et al. (J Complex 26(3):268–295, 2010). Applications to some special cases of Kantorovich–type conditions are also provided in this study.     

Deconvolution: a wavelet frame approach

This paper devotes to analyzing deconvolution algorithms based on wavelet frame approaches, which has already appeared in Chan et al. (SIAM J. Sci. Comput. 24(4), 1408–1432, 2003; Appl. Comput. Hormon. Anal. 17, 91–115, 2004a; Int. J. Imaging Syst. Technol. 14, 91–104, 2004b) as wavelet frame based high resolution image reconstruction methods. We first give a complete formulation of deconvolution in terms of multiresolution analysis and its approximation, which completes the formulation given in Chan et al. (SIAM J. Sci. Comput. 24(4), 1408–1432, 2003; Appl. Comput. Hormon. Anal. 17, 91–115, 2004a; Int. J. Imaging Syst. Technol. 14, 91–104, 2004b). This formulation converts deconvolution to a problem of filling the missing coefficients of wavelet frames which satisfy certain minimization properties. These missing coefficients are recovered iteratively together with a built-in denoising scheme that removes noise in the data set such that noise in the data will not blow up while iterating. This approach has already been proven to be efficient in solving various problems in high resolution image reconstructions as shown by the simulation results given in Chan et al. (SIAM J. Sci. Comput. 24(4), 1408–1432, 2003; Appl. Comput. Hormon. Anal. 17, 91–115, 2004a; Int. J. Imaging Syst. Technol. 14, 91–104, 2004b). However, an analysis of convergence as well as the stability of algorithms and the minimization properties of solutions were absent in those papers. This paper is to establish the theoretical foundation of this wavelet frame approach. In particular, a proof of convergence, an analysis of the stability of algorithms and a study of the minimization property of solutions are given.     

Labeled sequent calculi for modal logics and implicit contractions

The paper settles an open question concerning Negri-style labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s tree-hypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain complete w.r.t. valid sequents whose relational part encodes a tree-like structure, when the unique rule which contains an harmful implicit contraction—by which the condition that the premises be less complex than the conclusion is violated—is modified into a contraction-free one respecting the latter condition, thus making the proof-search space finite.     

Analysis of a class of nonlinear subdivision schemes and associated multiresolution transforms

This paper is devoted to the convergence and stability analysis of a class of nonlinear subdivision schemes and associated multiresolution transforms. As soon as a nonlinear scheme can be written as a specific perturbation of a linear and convergent subdivision scheme, we show that if some contractivity properties are satisfied, then stability and convergence can be achieved. This approach is applied to various schemes, which give different new results. More precisely, we study uncentered Lagrange interpolatory linear schemes, WENO scheme (Liu et al., J Comput Phys 115:200–212, 1994), PPH and Power-P schemes (Amat and Liandrat, Appl Comput Harmon Anal 18(2):198–206, 2005; Serna and Marquina, J Comput Phys 194:632–658, 2004) and a nonlinear scheme using local spherical coordinates (Aspert et al., Comput Aided Geom Des 20:165–187, 2003). Finally, a stability proof is given for the multiresolution transform associated to a nonlinear scheme of Marinov et al. (2005).     

Linguistic-based voting through centered OWA operators

Two linguistic-based voting systems have been introduced in recent years, namely: Majority Judgement (Balinski and Laraki in , 2007a) and Range Voting (Smith in , 2000). The keys for them are aggregation procedures based on the median and the arithmetic mean of the grades assessed to the alternatives, respectively. In this paper a comprehensive framework based on centered OWA operators (Yager in Soft Comput 11:631–639, 2007a) and the 2-tuple model (Herrera and Martínez in IEEE Trans Fuzzy Syst 8:746–752, 2000) is provided to enclose such distinct approaches. In addition, we show how to avoid some drawbacks of Majority Judgement and Range Voting by means of the use of suitable aggregation functions.     

Leibniz filters and the strong version of a protoalgebraic logic

A filter of a sentential logic ? is Leibniz when it is the smallest one among all the ?-filters on the same algebra having the same Leibniz congruence. This paper studies these filters and the sentential logic ?⁺ defined by the class of all ?-matrices whose filter is Leibniz, which is called the strong version of ?, in the context of protoalgebraic logics with theorems. Topics studied include an enhanced Correspondence Theorem, characterizations of the weak algebraizability of ?⁺ and of the explicit definability of Leibniz filters, and several theorems of transfer of metalogical properties from ? to ?⁺. For finitely equivalential logics stronger results are obtained. Besides the general theory, the paper examines the examples of modal logics, quantum logics and Łukasiewicz's finitely-valued logics. One finds that in some cases the existence of a weak and a strong version of a logic corresponds to well-known situations in the literature, such as the local and the global consequences for normal modal logics; while in others these constructions give an independent interest to the study of other lesser-known logics, such as the lattice-based many-valued logics. Received: 30 October 1998 /?Published online: 15 June 2001     

Multi-step nonlinear conjugate gradient methods for unconstrained minimization

Conjugate gradient methods are appealing for large scale nonlinear optimization problems, because they avoid the storage of matrices. Recently, seeking fast convergence of these methods, Dai and Liao (Appl. Math. Optim. 43:87–101, 2001) proposed a conjugate gradient method based on the secant condition of quasi-Newton methods, and later Yabe and Takano (Comput. Optim. Appl. 28:203–225, 2004) proposed another conjugate gradient method based on the modified secant condition. In this paper, we make use of a multi-step secant condition given by Ford and Moghrabi (Optim. Methods Softw. 2:357–370, 1993; J. Comput. Appl. Math. 50:305–323, 1994) and propose two new conjugate gradient methods based on this condition. The methods are shown to be globally convergent under certain assumptions. Numerical results are reported.     

Simultaneously inpainting in image and transformed domains

In this paper, we focus on the restoration of images that have incomplete data in either the image domain or the transformed domain or in both. The transform used can be any orthonormal or tight frame transforms such as orthonormal wavelets, tight framelets, the discrete Fourier transform, the Gabor transform, the discrete cosine transform, and the discrete local cosine transform. We propose an iterative algorithm that can restore the incomplete data in both domains simultaneously. We prove the convergence of the algorithm and derive the optimal properties of its limit. The algorithm generalizes, unifies, and simplifies the inpainting algorithm in image domains given in Cai et al. (Appl Comput Harmon Anal 24:131–149, 2008) and the inpainting algorithms in the transformed domains given in Cai et al. (SIAM J Sci Comput 30(3):1205–1227, 2008), Chan et al. (SIAM J Sci Comput 24:1408–1432, 2003; Appl Comput Harmon Anal 17:91–115, 2004). Finally, applications of the new algorithm to super-resolution image reconstruction with different zooms are presented. R. H. Chan’s research was supported in part by HKRGC Grant 400505 and CUHK DAG 2060257. L. Shen’s research was supported by the US National Science Foundation under grant DMS-0712827. Z. Shen’s research was supported in part by Grant R-146-000-060-112 at the National University of Singapore.     

Some new simple stability criteria of linear neutral systems with a single delay

This article mainly considers the linear neutral delay-differential systems with a single delay. Using the characteristic equation of the system, new simple delay-independent asymptotic and exponential stability criteria are derived in terms of the matrix measure, the spectral norm and the spectral radius of the corresponding matrices. Numerical examples demonstrate that our criteria are less conservative than those of previous corresponding results [L.M. Li, Stability of linear neutral delay-differential systems, Bull. Aust. Math. Soc. 38 (1988) 339–344; G.D. Hu, G.D. Hu. Some simple criteria for stability of neutral delay-differential systems, Appl. Math. Comput. 80 (1996) 257–271; D.Q. Cao, Ping He, Sufficient conditions for stability of linear neutral systems with a single delay, Appl. Math. Lett. 17 (2004) 139–144; G.D. Hu, G.D. Hu, B. Cahlon, Algebraic criteria for stability of linear neutral systems with a single delay, J. Comput. Appl. Math. 135 (2001) 125–130].